proposition: Lemma local_mon_imp_mon_le : forall n (f : forall i, i <= n -> R), (forall i H H', f i H [<] f (S i) H') -> forall i j Hi Hj, i < j -> f i Hi [<] f j Hj.
proof: Proof. simple induction j. intros Hi Hj H0; exfalso; inversion H0. clear j; intro j; intros. elim (le_lt_eq_dec _ _ H); intro. cut (j <= n); [ intro | auto with arith ]. apply leEq_less_trans with (f j H0). apply less_leEq; auto with arith. apply X. generalize Hj; rewrite <- b. auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)