proposition: Theorem plus_id_exercise : forall n m o : nat, n = m -> m = o -> n + m = m + o.
proof: Proof. Admitted. Check mult_n_O. Check mult_n_Sm. Theorem mult_n_0_m_0 : forall p q : nat, (p * 0) + (q * 0) = 0. Proof. intros p q. rewrite <- mult_n_O. rewrite <- mult_n_O. reflexivity. Qed.