1 (* for 2D hexagon perimeter theorem *)
3 let ell_uvx = new_definition `ell_uvx (x1:real) (x2:real) (x3:real)
4 (x4:real) (x5:real) (x6:real) =
5 (let et2 = eta_x x1 x2 x3 pow 2 in
6 sqrt(et2 - (x1/ &4)) + sqrt(et2 - (x2/ &4)))`;;
8 let ell_vx2 = new_definition `ell_vx2 (x1:real) (x2:real) (x3:real)
9 (x4:real) (x5:real) (x6:real) =
10 (let et2 = eta_x x1 x2 x3 pow 2 in
11 sqrt(et2 - (x2/ &4)))`;;