loads "/home/ky/flyspeck/working/REUHADY.hl";;
loads "/home/ky/flyspeck/working/TSKAJXY_lemmas.hl";;

let h0cut = new_definition `h0cut y = if (y <= &2 * h0) then &1 else &0`;;

let cell3_from_ineq = 
 `!y4 y5 y6.
         &2 <= y4 /\
         &2 <= y5 /\
         &2 <= y6 /\
         y4 <= &2 * sqrt (&2) /\
         y5 <= &2 * sqrt (&2) /\
         y6 <= &2 * sqrt (&2) /\
         eta_y y4 y5 y6 < sqrt (&2)
         ==> &0 <= gamma3f y4 y5 y6 sqrt2 lmfun`;;

let GRKIBMP_concl = 
  `!y. &2 <= y /\ y <= sqrt8 ==>
     &0 <= gamma2_x_div_azim (h0cut y) (y*y)`;;

let tsk_hyp_new = mk_conj(GRKIBMP_concl, 
                              mk_conj(cell3_from_ineq,tsk_hyp));;