(* for 2D hexagon perimeter theorem *)

let ell_uvx = new_definition `ell_uvx (x1:real) (x2:real) (x3:real)
  (x4:real) (x5:real) (x6:real) = 
  (let et2 = eta_x x1 x2 x3 pow 2 in
     sqrt(et2 - (x1/ &4)) + sqrt(et2 - (x2/ &4)))`;;
let ell_vx2 = new_definition `ell_vx2 (x1:real) (x2:real) (x3:real)
  (x4:real) (x5:real) (x6:real) = 
  (let et2 = eta_x x1 x2 x3 pow 2 in
     sqrt(et2 - (x2/ &4)))`;;