proposition: Lemma lt_succ_diag_r p : p < succ p.
proof: Proof. rewrite lt_iff_add. exists 1. apply add_1_r. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef