proposition: Lemma pred_N_succ p : pred_N (succ p) = Npos p.
proof: Proof. destruct p; simpl; trivial. f_equal. apply pred_double_succ. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef