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