proposition: Lemma succ_inj p q : succ p = succ q -> p = q.
proof: Proof. revert q. induction p as [p|p|]; intros [q|q| ] H; simpl in H; destr_eq H; f_equal; auto. - elim (succ_not_1 p); auto. - elim (succ_not_1 q); auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef