proposition: Lemma lognat_correct2 : forall(a : nat)(pf : a <> 0), a < (expnat 2 (S (lognat pf))).
proof: Proof. intros. simpl. rewrite fold_add. assert (expnat 2 (lognat pf) <> 0). apply expnat_nz. auto. assert (2 * (expnat 2 (lognat pf)) <> 0). lia. eapply (lognat_ge_monotonic_mt pf H0). rewrite <- (lognat_prod_sum H). rewrite lognat_correct_eq. lia. Qed.
imports: ZArith micromega.Lia