proposition: Lemma resp_leEq_char : forall (f : R -> R) x y, (x [=] y -> f x [=] f y) -> (x [<] y -> f x [<] f y) -> x [<=] y -> f x [<=] f y.
proof: Proof. intros. set (f' := fun (x : R) (H : True) => f x) in *. change (f' x I [<=] f' y I) in |- *. apply resp_leEq_char' with (P := fun x : R => True); auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)