proposition: Lemma mult_resp_pos : forall x y : F, [0] [<] x -> [0] [<] y -> [0] [<] x[*]y.
proof: Proof. elim COrdField_is_COrdField; auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)