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