1 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
4 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
6 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
9 e(CONV_TAC ARITH_RULE);;
10 let trivial = top_thm();;
12 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
13 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]));;
15 e(ONCE_REWRITE_TAC[EQ_SYM_EQ]);;
17 e(ASM_REWRITE_TAC[]);;
18 e(CONV_TAC ARITH_RULE);;
19 let trivial = top_thm();;
21 g `2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`;;
22 e(CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
23 SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
24 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
25 let trivial = top_thm();;
28 (`2 <= n /\ n <= 2 ==> f(2,2) + n < f(n,n) + 7`,
29 CONV_TAC(REWRITE_CONV[LE_ANTISYM]) THEN
30 SIMP_TAC[] THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] THEN
31 DISCH_TAC THEN ASM_REWRITE_TAC[] THEN CONV_TAC ARITH_RULE);;
34 (`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
35 REPEAT GEN_TAC THEN MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN
36 MP_TAC(SPECL [`x:real`; `--y`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
39 (`!x y:real. &0 < x * y ==> (&0 < x <=> &0 < y)`,
40 MATCH_MP_TAC REAL_WLOG_LE THEN CONJ_TAC THEN REPEAT GEN_TAC THEN
41 MP_TAC(SPECL [`--x`; `y:real`] REAL_LE_MUL) THEN REAL_ARITH_TAC);;
43 let SUM_OF_NUMBERS = prove
44 (`!n. nsum(1..n) (\i. i) = (n * (n + 1)) DIV 2`,
45 INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
47 let SUM_OF_SQUARES = prove
48 (`!n. nsum(1..n) (\i. i * i) = (n * (n + 1) * (2 * n + 1)) DIV 6`,
49 INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;
51 let SUM_OF_CUBES = prove
52 (`!n. nsum(1..n) (\i. i*i*i) = (n * n * (n + 1) * (n + 1)) DIV 4`,
53 INDUCT_TAC THEN ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG] THEN ARITH_TAC);;