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