proposition: Theorem plus_comm' : forall n m : nat, n + m = m + n.
proof: Proof. induction n as [| n']. - intros m. rewrite <- plus_n_O. reflexivity. - intros m. simpl. rewrite -> IHn'. rewrite <- plus_n_Sm. reflexivity. Qed.
imports: ProofObjects