proposition: Lemma local_mon_imp_mon' : forall f : nat -> R, (forall i, f i [<] f (S i)) -> 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 local_mon_imp_mon with (f := f); assumption. apply eq_imp_leEq; rewrite b; algebra. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)