proposition: Lemma lt_mono_imp_le_mono f (LTM: forall n m, n < m -> f n < f m): forall n m, n <= m -> f n <= f m.
proof: Proof. intros n m H. induction H. - constructor. - eapply le_trans. exact IHle. apply lt_le_incl, LTM, lt_succ_diag_r. Qed.
imports: Arith Lia Equations(Equations)