proposition: Lemma Greater_imp_ap : forall x y : R, y [<] x -> x [#] y.
proof: Proof. intros x y H. elim (less_conf_ap _ x y); intros. apply b. right. auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)