proposition: Lemma equal_less_leEq : forall a b x y : R, (a [<] b -> x [<=] y) -> (a [=] b -> x [<=] y) -> a [<=] b -> x [<=] y.
proof: Proof. intros. rewrite -> leEq_def. red in |- *. apply CNot_Not_or with (a [<] b) (a [=] b). firstorder using leEq_def. firstorder using leEq_def. intro. cut (a [=] b); intros. 2: apply leEq_imp_eq; auto. auto. rewrite -> leEq_def. intro; auto. Qed.
imports: CoRN.algebra.COrdFields Coq(Lia)