Example (21.2)

　４変数から３変数の場合を導きましょう．まず，lemmaを用意します．

g`!x. &0 <= x ==> root 3 x = root 4 ( root 3 x * x )`;;
e(SIMP_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC);;
e(ASM_SIMP_TAC[ARITH_RULE`3 = SUC 2 /\ 4 = SUC 3`; REAL_EXP_POS_LT; REAL_LT_MUL; ROOT_LN; REAL_EXP_INJ]);;
e(NUM_REDUCE_TAC THEN ASM_SIMP_TAC[REAL_ARITH`x / &3 = y / &4 <=> &4 * x = &3 * y`; REAL_EXP_POS_LT; REAL_LT_MUL; GSYM LN_POW]);;
e(ASM_SIMP_TAC[POW_MUL; ARITH_RULE`3 = SUC 2`; ROOT_LT_LEMMA;]);;
e(NUM_REDUCE_TAC THEN AP_TERM_TAC THEN CONV_TAC REAL_RING);;
e(FIRST_ASSUM (MP_TAC o GSYM) THEN SIMP_TAC[ARITH_RULE`4 = SUC 3 /\ 3 = SUC 2`; ROOT_0; REAL_MUL_RZERO]);;
let root3 = top_thm();;

　本体です．

# g`!a b c. &0 <= a /\ &0 <= b /\ &0 <= c ==> (a + b + c) / &3 >= root 3 (a * b * c)`;;
val it : goalstack = 1 subgoal (1 total)

`!a b c.
     &0 <= a /\ &0 <= b /\ &0 <= c ==> (a + b + c) / &3 >= root 3 (a * b * c)`

# e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 <= a`]
  1 [`&0 <= b`]
  2 [`&0 <= c`]

`(a + b + c) / &3 >= root 3 (a * b * c)`

# e(SUBGOAL_THEN `&0 <= a * b * c` ASSUME_TAC THENL [ASM_SIMP_TAC[REAL_LE_MUL]; ALL_TAC]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 <= a`]
  1 [`&0 <= b`]
  2 [`&0 <= c`]
  3 [`&0 <= a * b * c`]

`(a + b + c) / &3 >= root 3 (a * b * c)`

# (*
  e(REPEAT GEN_TAC);;
  e(DISCH_THEN(fun t -> ASSUME_TAC(CONJ t (MESON[t;REAL_LE_MUL]`&0 <= a * b * c`))));;
  *)
  e(MP_TAC (SPECL[`root 3 (a * b * c)`;`a:real`;`b:real`;`c:real`]amgm4) THEN
    ASM_SIMP_TAC[ARITH_RULE`3 = SUC 2`; ROOT_POS_POSITIVE; GSYM root3]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 <= a`]
  1 [`&0 <= b`]
  2 [`&0 <= c`]
  3 [`&0 <= a * b * c`]

`(root (SUC 2) (a * b * c) + a + b + c) / &4 >= root (SUC 2) (a * b * c)
 ==> (a + b + c) / &(SUC 2) >= root (SUC 2) (a * b * c)`

# e(NUM_REDUCE_TAC THEN REAL_ARITH_TAC);;
val it : goalstack = No subgoals

# let amgm3 = top_thm();;
val amgm3 : thm =
  |- !a b c.
         &0 <= a /\ &0 <= b /\ &0 <= c
         ==> (a + b + c) / &3 >= root 3 (a * b * c)

　なお，２変数の場合をSQRT_SOSを用いずに証明するなら，例えば

# (* amgm2 alt *)
  g`!a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt(a * b)`;;
val it : goalstack = 1 subgoal (1 total)

`!a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt (a * b)`

# e(REPEAT STRIP_TAC);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 <= a`]
  1 [`&0 <= b`]

`(a + b) / &2 >= sqrt (a * b)`

# e(MP_TAC (SPEC`sqrt a - sqrt b`REAL_LE_POW_2));;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 <= a`]
  1 [`&0 <= b`]

`&0 <= (sqrt a - sqrt b) pow 2 ==> (a + b) / &2 >= sqrt (a * b)`

# e(ASM_SIMP_TAC[REAL_POLY_CONV`(x - y) pow 2`; SQRT_POW_2; SQRT_MUL]);;
val it : goalstack = 1 subgoal (1 total)

  0 [`&0 <= a`]
  1 [`&0 <= b`]

`&0 <= a + -- &2 * sqrt a * sqrt b + b ==> (a + b) / &2 >= sqrt a * sqrt b`

# e(REAL_ARITH_TAC);;
val it : goalstack = No subgoals

# let amgm2 = top_thm();;
val amgm2 : thm =
  |- !a b. &0 <= a /\ &0 <= b ==> (a + b) / &2 >= sqrt (a * b)

となります．