proposition: Theorem pred_succ n : pred (succ n) = n.
proof: Proof. destruct n; trivial. simpl. apply Pos.pred_N_succ. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties