# 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