1 let neg_odd_lem = prove_by_refinement(
3 (a pow n * p x = c x * q x + d x) ==>
5 ((-- a) pow n * p x = (-- c x) * q x + (-- d x))`,
10 REWRITE_TAC[REAL_ARITH `-- x * y = -- (x * y)`];
11 REWRITE_TAC[REAL_ARITH `-- x + -- y = -- (x + y)`];
12 CLAIM `-- a pow n = -- (a pow n)`;
13 DISJ_CASES_TAC (ARITH_RULE `a < &0 \/ (a = &0) \/ a > &0`);
14 MP_TAC (ISPECL[`a:real`;`n:num`] REAL_POW_NEG);
15 ASM_REWRITE_TAC[GSYM NOT_ODD];
16 POP_ASSUM DISJ_CASES_TAC;
17 ASM_REWRITE_TAC[real_pow];
21 CLAIM `?n'. n = SUC n'`;
22 ASM_MESON_TAC[num_CASES];
24 ASM_REWRITE_TAC[real_pow];
26 MP_TAC (ISPECL[`a:real`;`n:num`] REAL_POW_NEG);
27 ASM_REWRITE_TAC[GSYM NOT_ODD];
30 REWRITE_TAC[ARITH_RULE `-- x * y = -- (x * y)`];
31 REWRITE_TAC[ARITH_RULE `(-- x = -- y) <=> (x = y)`];
32 FIRST_ASSUM MATCH_ACCEPT_TAC;
37 let mul_odd_lem = prove_by_refinement(
39 (a pow n * p x = c x * q x + d x) ==>
41 ((a * a pow n) * p x = (a * c x) * q x + (a * d x))`,
45 REWRITE_TAC[REAL_ARITH `(a * x) * y = a * (x * y)`];
46 REWRITE_TAC[REAL_ARITH `a * x + a * y = a * (x + y)`];
48 FIRST_ASSUM MATCH_ACCEPT_TAC;