1 loads "/home/ky/flyspeck/working/REUHADY.hl";;
2 loads "/home/ky/flyspeck/working/TSKAJXY_lemmas.hl";;
4 let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;
12 y4 <= &2 * sqrt (&2) /\
13 y5 <= &2 * sqrt (&2) /\
14 y6 <= &2 * sqrt (&2) /\
15 eta_y y4 y5 y6 < sqrt (&2)
16 ==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;
19 `!y. &2 <= y /\ y <= sqrt8 ==>
20 &0 <= gamma2_x_div_azim (h0cut y) (y*y)`;;
22 let tsk_hyp_new = mk_conj(GRKIBMP_concl,
23 mk_conj(cell3_from_ineq,tsk_hyp));;