proposition: Theorem plus_id_exercise : forall n m o : nat, n = m -> m = o -> n + m = m + o.
proof: Proof. MProof. Admitted. Theorem mult_0_plus : forall n m : nat, (0 + n) * m = n * m. MProof. intros n m. rewrite -> plus_O_n. reflexivity. Qed.