proposition: Lemma leEq_or_leEq : forall x y:R, Not (Not (x[<=]y or y[<=]x)).
proof: Proof. intros x y H. apply H. right. rewrite -> leEq_def. intros H0. apply H. left. apply less_leEq. assumption. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)