proposition: Theorem mul_succ_l n m : (succ n) * m = n * m + m.
proof: Proof. destruct n, m; simpl; trivial. f_equal. rewrite Pos.add_comm. apply Pos.mul_succ_l. Qed.
imports: BinNums BinPos RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties