proposition: Lemma minus_resp_leEq_rht : forall x y z : R, y [<=] x -> z[-]x [<=] z[-]y.
proof: Proof. intros. Transparent cg_minus. unfold cg_minus in |- *. apply plus_resp_leEq_lft. apply inv_resp_leEq. assumption. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)