不等式

# prove(
   `!a b c A B C. &0 < a /\ a <= b /\ b <= c /\ c < a + b /\ &0 < A /\ A <= B /\ B
 <= C /\ A + B + C = &180 ==> &60 <= (a * A + b * B + c * C) / (a + b + c) /\ (a *
 A + b * B + c * C) / (a + b + c) < &90`,
    REPEAT STRIP_TAC THEN
    REWRITE_TAC[REAL_ARITH `&60 = &180 / &3`;REAL_ARITH `&90 = &180 / &2`] THEN
    POP_ASSUM (SUBST1_TAC o GSYM) THENL
   [MATCH_MP_TAC REAL_LE_RDIV THEN
    SUBGOAL_TAC "" `&0 <= (c - b) * (C - B) /\ &0 <= (c - a) * (C - A) /\ &0 <= (b
 - a) * (B - A)` [ASM_MESON_TAC[REAL_SUB_LE;REAL_LE_TRANS;REAL_LE_MUL]];
    MATCH_MP_TAC (MESON[REAL_LT_LDIV_EQ]`&0 < y /\ x < c * y ==> x / y < c`) THEN
    SUBGOAL_TAC "" `a < b + c /\ b < c + a /\ &0 < B /\ &0 < C` [ASM_REAL_ARITH_TA
C] THEN
    SUBGOAL_TAC "" `a * A < (b + c) * A /\ b * B < (c + a) * B /\ c * C < (a + b)
* C` [ASM_MESON_TAC[REAL_LT_RMUL]]] THEN
    ASM_REAL_ARITH_TAC);;
0..0..1..2..solved at 6
0..0..1..3..8..15..24..solved at 61
0..0..1..3..8..15..24..58..121..221..421..816..1606..solved at 3345
0..0..1..3..8..15..24..solved at 61
0..0..1..2..solved at 6
0..0..1..2..solved at 6
0..0..1..2..solved at 6
val it : thm =
  |- !a b c A B C.
         &0 < a /\
         a <= b /\
         b <= c /\
         c < a + b /\
         &0 < A /\
         A <= B /\
         B <= C /\
         A + B + C = &180
         ==> &60 <= (a * A + b * B + c * C) / (a + b + c) /\
             (a * A + b * B + c * C) / (a + b + c) < &90