proposition: Lemma compare_cont_Gt_not_Lt p q : compare_cont Gt p q <> Lt <-> p >= q.
proof: Proof. apply not_iff_compat, compare_cont_Gt_Lt. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef