Skip to content

Instantly share code, notes, and snippets.

@pi8027

pi8027/gist:9515d59d6c75b2fc3f1177fff08dfe31

Last active July 20, 2016 05:14
Show Gist options
  • Save pi8027/9515d59d6c75b2fc3f1177fff08dfe31 to your computer and use it in GitHub Desktop.
Save pi8027/9515d59d6c75b2fc3f1177fff08dfe31 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
gistfile1.txt
Require Import mathcomp.ssreflect.all_ssreflect.
Goal forall p k n, 1 < p -> p ^ k <= n < p ^ k.+1 -> trunc_log p n = k.
Proof.
move => p k n H /andP [H0 H1].
have/(trunc_log_bounds H)/andP [H2 _] : 0 < n
by apply: (leq_trans _ H0); rewrite expn_gt0 (ltnW H).
apply/eqP; rewrite eqn_leq trunc_log_max // andbT.
move: H1; apply contraTT; rewrite -leqNgt -ltnNge => H1.
by apply: (leq_trans _ H2); rewrite leq_exp2l.
Qed.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment