Require Import Arith.
Require Import Omega.
Open Scope Z_scope.
Theorem t: forall n:Z, n*n - 2*n + 1 = (n-1)*(n-1).
intros.
symmetry.
replace ((n-1)*(n-1)) with (n*(n-1)-1*(n-1)).
replace (1*(n-1)) with (n-1).
replace (n*(n-1)) with (n*n-n).
replace (n*n-n-(n-1)) with (n*n-(n-1)-n).
replace (n*n-(n-1)) with (n*n-n+1).
replace (n*n-n+1-n) with (n*n-n-n+1).
replace (n*n-n-n) with (n*n-2*n).
omega.
omega.
omega.
omega.
omega.
symmetry.
replace (n*n-n) with (n*n-n*1).
apply Z.mul_sub_distr_l.
omega.
symmetry.
apply Z.mul_sub_distr_r.
Qed.