proposition: Lemma lognat_ge_monotonic : forall (a b : nat)(pfa : a <> 0)(pfb : b <> 0), a >= b -> (lognat pfa) >= (lognat pfb).
proof: Proof. intros. remember (a - b) as c. apply (@lognat_ge_monotonic_h c); auto. Qed.
imports: ZArith micromega.Lia