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