proposition: Lemma resp_less_char' : forall (P : R -> CProp) (f : forall x, 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. elim (ap_imp_less _ _ _ (X (less_imp_ap _ _ _ X0))); intros. auto. exfalso. apply less_irreflexive_unfolded with (x := f x Hx). apply leEq_less_trans with (f y Hy); auto. apply H; apply less_leEq; auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)