proposition: Lemma succ_pred_or p : p = 1 \/ succ (pred p) = p.
proof: Proof. destruct p; simpl; auto. right; apply succ_pred_double. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef