proposition: Lemma succ_pred p : p <> 1 -> succ (pred p) = p.
proof: Proof. destruct p; intros H; simpl; trivial. - apply succ_pred_double. - now destruct H. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef