-を+に変えた版はできた。
-の方はまだできてない。

Require Import Omega.
Require Import Arith.
Theorem t:forall n:nat,n*n+2*n+1=(n+1)*(n+1).
intros.
replace (2*n) with (n+n).
symmetry.
replace ((n+1)*(n+1)) with (n*(n+1)+1*(n+1)).
replace (n*(n+1)) with (n*n+n*1).
omega.
symmetry.
apply mult_plus_distr_l.
symmetry.
apply mult_plus_distr_r.
omega.
Qed.