proposition: Lemma minus_resp_less_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_less_lft. apply inv_resp_less. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)