equal
deleted
inserted
replaced
11 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
11 Thanks to Sloane's On-Line Encyclopedia of Integer Sequences, |
12 http://www.research.att.com/~njas/sequences/ |
12 http://www.research.att.com/~njas/sequences/ |
13 *) |
13 *) |
14 |
14 |
15 Addsimps [add_mult_distrib, add_mult_distrib2]; |
15 Addsimps [add_mult_distrib, add_mult_distrib2]; |
|
16 Addsimps [diff_mult_distrib, diff_mult_distrib2]; |
16 |
17 |
17 (*The sum of the first n odd numbers equals n squared.*) |
18 (*The sum of the first n odd numbers equals n squared.*) |
18 Goal "sum (%i. Suc(i+i)) n = n*n"; |
19 Goal "sum (%i. Suc(i+i)) n = n*n"; |
19 by (induct_tac "n" 1); |
20 by (induct_tac "n" 1); |
20 by Auto_tac; |
21 by Auto_tac; |