equal
deleted
inserted
replaced
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)" |
86 lemma "(n - 1) * (n + 1) = n * n - (1::nat)" |
87 apply (clarsimp split: nat_diff_split) |
87 apply (clarsimp split: nat_diff_split iff del: less_Suc0) |
88 --{* @{subgoals[display,indent=0,margin=65]} *} |
88 --{* @{subgoals[display,indent=0,margin=65]} *} |
89 apply (subgoal_tac "n=0", force, arith) |
89 apply (subgoal_tac "n=0", force, arith) |
90 done |
90 done |
91 |
91 |
92 |
92 |