proposition: Lemma local_mon'_imp_mon'2_lt : 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. intros; induction j as [| j Hrecj]. exfalso; inversion H0. elim (le_lt_eq_dec _ _ H0); intro. cut (j < n); [ intro | auto with arith ]. apply leEq_transitive with (f j H1). apply Hrecj; auto with arith. apply H. generalize Hj; rewrite <- b. intro; apply H. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)