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. simple induction j. intros H0; exfalso; inversion H0. clear j; intro j; intros H0 H1. elim (le_lt_eq_dec _ _ H1); intro. apply leEq_less_trans with (f j). apply less_leEq; apply H0; auto with arith. auto. rewrite <- b; apply X. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)