proposition: Lemma ge_not_lt x y : y<=x -> x<y -> False.
proof: Proof. intros H H'. apply (StrictOrder_Irreflexive x). rewrite le_lteq in *; destruct H as [H|H]. - transitivity y; auto. - rewrite H in H'; auto. Qed.
imports: Orders OrdersTac OrdersFacts Setoid Morphisms Basics