proposition: Lemma resp_less_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_less_char' with (P := fun x : R => True); auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)