proposition: Lemma mono_weak f (H: mono f) : forall n p, n <= p -> f n <= f p.
proof: Proof. induction 1. left. auto. transitivity (f m); auto. Search lt le. apply PeanoNat.Nat.lt_le_incl; apply H;auto. Qed.
imports: Coq(ArithRing Lia Arith)