proposition: Lemma part_mon_imp_mon' : forall F (I : R -> CProp), (forall x, I x -> Dom F x) -> (forall x y Hx Hy, I x -> I y -> x [<] y -> F x Hx [<] F y Hy) -> forall x y Hx Hy, I x -> I y -> x [<=] y -> F x Hx [<=] F y Hy.
proof: Proof. intros. rewrite -> leEq_def. intro. cut (x [=] y); intros. apply (less_irreflexive_unfolded _ (F x Hx)). astepl (F y Hy); auto. apply leEq_imp_eq. firstorder using leEq_def. rewrite -> leEq_def. intro. apply (less_irreflexive_unfolded _ (F x Hx)). apply less_transitive_unfolded with (F y Hy); firstorder using leEq_def. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)