g `!s t a b. &0<=s /\ &0<=t /\ s+t= &1 /\ &0<=a /\ &0<=b /\ a<=b ==> !n. (s*a+t*b) pow n <= s*a pow n + t*b pow n` ;;
e( REPEAT GEN_TAC THEN STRIP_TAC );;
e( INDUCT_TAC );;
e( ASM_REAL_ARITH_TAC );;
e( REWRITE_TAC [pow] );;
let lem1 = MESON [REAL_LE_MUL;REAL_LE_ADD] `&0 <= s ==> &0 <= t ==> &0 <= a ==> &0 <= b ==> &0 <= s*a + t*b`;;
let lem2 = SPECL [`s*a + t*b:real`; `(s*a + t*b) pow n`;`s*a pow n + t*b pow n`] REAL_LE_LMUL;;
e( SUBGOAL_THEN `(s*a + t*b) * (s*a pow n + t*b pow n) <= s*a * a pow n + t*b * b pow n` (fun t -> MAP_EVERY MP_TAC [t;lem1;lem2] THEN ASM_MESON_TAC [REAL_LE_TRANS] ) );;
e( ONCE_REWRITE_TAC [GSYM REAL_SUB_LE] );;
e( REWRITE_TAC [UNDISCH(REAL_RING `s+t= &1==>(s * a * x + t * b * y) - (s * a + t * b) * (s * x + t * y)=s*t*(b-a)*(y-x)`) ] );;
e( ASM_MESON_TAC [POW_LE;REAL_SUB_LE;REAL_LE_MUL] );;
let theorem_20130313 = MESON [top_thm (); REAL_LE_TOTAL; REAL_ADD_SYM] `!s t a b. &0<=s /\ &0<=t /\ s+t= &1 /\ &0<=a /\ &0<=b ==> !n. (s*a+t*b) pow n <= s*a pow n + t*b pow n` ;;
