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; induction j as [| j Hrecj]. cut (i = 0); [ intro | auto with arith ]. rewrite H1; apply leEq_reflexive. elim (le_lt_eq_dec _ _ H0); intro. apply leEq_transitive with (f j). apply Hrecj; auto with arith. apply H. rewrite b; apply leEq_reflexive. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)