proposition: Lemma leEq_not_eq : forall x y : R, x [<=] y -> x [#] y -> x [<] y.
proof: Proof. intros x y H H0. elim (ap_imp_less _ _ H0); intro H1; auto. rewrite -> leEq_def in H. elim (H H1). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)