proposition: Lemma lognat_odd : forall(a : nat)(pf1 : (2 * a) <> 0)(pf2 : (S (2 * a)) <> 0), ((lognat pf2) = (lognat pf1)).
proof: Proof. intros. unfold lognat in *. rewrite (factor_s_conv pf1 pf2). assert (a <> 0). lia. rewrite (factor_double_conv H pf1). simpl. auto. Qed.
imports: ZArith micromega.Lia