proposition: Lemma resp_leEq_char' : forall (P : R -> CProp) (f : forall x : R, P x -> R) x y Hx Hy, (x [=] y -> f x Hx [=] f y Hy) -> (x [<] y -> f x Hx [<] f y Hy) -> x [<=] y -> f x Hx [<=] f y Hy.
proof: Proof. intros. rewrite -> leEq_def. intro. cut (Not (x [<] y) /\ ~ x [=] y); intros. inversion_clear H1. apply H3. apply leEq_imp_eq; firstorder using leEq_def. split; intro. apply less_irreflexive_unfolded with (x := f y Hy). apply less_transitive_unfolded with (f x Hx); auto. apply less_irreflexive_unfolded with (x := f y Hy). apply less_leEq_trans with (f x Hx); auto. apply eq_imp_leEq; auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)