proposition: Theorem lt_succ_r p q : p < succ q <-> p <= q.
proof: Proof. unfold lt, le. generalize (compare_succ_r p q). do 2 destruct compare; try discriminate; now split. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef