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