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