# 不等式

# 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