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