proposition: Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
proof: Proof. intros x y; rewrite 2 P.le_lteq. intuition auto with relations. elim (StrictOrder_Irreflexive x); transitivity y; auto. Qed.
imports: Setoid Morphisms Basics Equalities Orders