proposition: Lemma lognat_0_1 : forall n (pf : n <> 0), lognat pf = 0 -> n = 1.
proof: Proof. intros. destruct n. lia. destruct n. trivial. assert (2 <> 0). lia. assert (lognat pf >= lognat H0). eapply lognat_ge_monotonic. lia. unfold lognat in *. simpl in *. lia. Qed.
imports: ZArith micromega.Lia