proposition: Theorem mult_0_r : forall n:nat, n * 0 = 0.
proof: Proof. MProof. Admitted. Theorem plus_n_Sm : forall n m : nat, S (n + m) = n + (S m). MProof. Admitted. Theorem plus_comm : forall n m : nat, n + m = m + n. MProof. Admitted. Theorem plus_assoc : forall n m p : nat, n + (m + p) = (n + m) + p. MProof. Admitted. Fixpoint double (n:nat) := match n with | O => O | S n' => S (S (double n')) end. Lemma double_plus : forall n, double n = n + n . MProof. Admitted. Theorem evenb_S : forall n : nat, evenb (S n) = negb (evenb n). MProof. Admitted. Theorem mult_0_plus' : forall n m : nat, (0 + n) * m = n * m. MProof. intros n m. assert (H: 0 + n = n). { reflexivity. } rewrite -> H. reflexivity. Qed.