proposition: Lemma mon_imp_mon' : forall f : nat -> R, (forall i j, i < j -> f i [<] f j) -> forall i j, i <= j -> f i [<=] f j.
proof: Proof. intros f H i j H0. elim (le_lt_eq_dec _ _ H0); intro. apply less_leEq; apply H; assumption. rewrite b; apply leEq_reflexive. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)