proposition: Lemma succ_pos_pred p : succ (Pos.pred_N p) = pos p.
proof: Proof. destruct p; simpl; trivial. f_equal. apply Pos.succ_pred_double. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties