proposition: Lemma lognat_ge_monotonic_h : forall (c a b : nat)(pfa : a <> 0)(pfb : b <> 0), a >= b -> c = (a - b) -> (lognat pfa) >= (lognat pfb).
proof: Proof. induction c. intros. assert (a = b) by intuition. subst. auto. intros. assert (a >= (S b)) by lia. assert (c = a - (S b)) by lia. eapply ge_trans. apply (IHc a (S b) pfa (s_nat_nz pfb)). apply H1. apply H2. apply lognat_ge_monotonic_b. Qed.
imports: ZArith micromega.Lia