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