proposition: Theorem lognat_correct_eq : forall(b : nat)(pf : (expnat 2 b) <> 0), (lognat pf) = b.
proof: Proof. induction b. intros. simpl in *. auto. intros. specialize (lognat_prod_sum (expnat_2_nz b)). intros. specialize (IHb (expnat_2_nz b)). rewrite IHb in H. symmetry in H. simpl in *. apply H. Qed.
imports: ZArith micromega.Lia