proposition: Lemma le_antisym p q : p <= q -> q <= p -> p = q.
proof: Proof. rewrite le_lteq; destruct 1; auto. rewrite le_lteq; destruct 1; auto. elim (lt_irrefl p). now transitivity q. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef