(* 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)))`;;