proposition: Lemma Dcompare : forall r:comparison, r = Eq \/ r = Lt \/ r = Gt.
proof: Proof. intro r; destruct r; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef