proposition: Lemma pos_pred_succ n : Pos.pred_N (succ_pos n) = n.
proof: Proof. destruct n. - trivial. - apply Pos.pred_N_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties