proposition: Lemma compare_cont_Lt_Gt p q : compare_cont Lt p q = Gt <-> p > q.
proof: Proof. rewrite compare_cont_spec. unfold gt. destruct (p ?= q); now split. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef