proposition: Lemma minus_resp_less : forall x y z : R, x [<] y -> x[-]z [<] y[-]z.
proof: Proof. Transparent cg_minus. unfold cg_minus in |- *. intros x y z H. apply plus_resp_less_rht. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)