proposition: Lemma lt_total p q : p < q \/ p = q \/ q < p.
proof: Proof. case (compare_spec p q); intuition. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef