equal
deleted
inserted
replaced
81 @{thm[display] nat_diff_split[no_vars]} |
81 @{thm[display] nat_diff_split[no_vars]} |
82 \rulename{nat_diff_split} |
82 \rulename{nat_diff_split} |
83 *} |
83 *} |
84 |
84 |
85 |
85 |
|
86 lemma "(n - 1) * (n + 1) = n * n - (1::nat)" |
|
87 apply (clarsimp split: nat_diff_split) |
|
88 --{* @{subgoals[display,indent=0,margin=65]} *} |
|
89 apply (subgoal_tac "n=0", force, arith) |
|
90 done |
|
91 |
|
92 |
86 lemma "(n - 2) * (n + 2) = n * n - (4::nat)" |
93 lemma "(n - 2) * (n + 2) = n * n - (4::nat)" |
87 apply (clarsimp split: nat_diff_split) |
94 apply (simp split: nat_diff_split, clarify) |
88 --{* @{subgoals[display,indent=0,margin=65]} *} |
95 --{* @{subgoals[display,indent=0,margin=65]} *} |
89 apply (subgoal_tac "n=0 | n=1", force, arith) |
96 apply (subgoal_tac "n=0 | n=1", force, arith) |
90 done |
97 done |
91 |
98 |
92 text{* |
99 text{* |