proposition: Lemma exp2_log2_prop : forall n p, log2_prop n p -> exp2 (S p) > n.
proof: Proof. cut(forall n n' p, n'<=n -> log2_prop n' p -> exp2 (S p) > n'). intros. eapply H. assert (n<=n). lia. ehyp. hyp. intro; induction n; intros. assert (n'=0). lia. subst. apply exp2_pos. inversion H; auto. subst; inversion H0. simpl; auto. subst. assert (exp2 (S q) > Nat.div2 (S n)). apply IHn. simpl; destruct n; auto with *. assert (Nat.div2 n <= n); auto with *. apply div2_le_n. hyp. change (2*exp2 (S q) > S n). gen(double_div2 (S n)); intro; lia. Qed.
imports: Coq(Lia PeanoNat) CoLoR(LogicUtil NatCompat)