proposition: Theorem lognat_correct : forall(a : nat)(pf : a <> 0), (expnat 2 (lognat pf)) <= a < (expnat 2 (S (lognat pf))).
proof: Proof. intros. split. remember (lognat pf) as b. apply (lognat_correct1 pf). auto. apply lognat_correct2. Qed.
imports: ZArith micromega.Lia