proposition: Lemma minus_resp_less_leEq : forall x y x' y' : R, x [<=] y -> y' [<] x' -> x[-]x' [<] y[-]y'.
proof: Proof. intros. astepl (x[+][--]x'). astepr (y[+][--]y'). apply plus_resp_leEq_less. auto. apply inv_resp_less. auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)