proposition: Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
proof: Proof. intros x y H. destruct (P.lt_total x y); auto. destruct H. rewrite P.le_lteq. intuition auto with relations. Qed.
imports: Setoid Morphisms Basics Equalities Orders