| destruct /3 width=2 by gget_eq, ex_intro/
| @ex_intro [2: @gget_gt normalize /2 width=1 by/ | skip ] (**) (* explicit constructor *)
]
| destruct /3 width=2 by gget_eq, ex_intro/
| @ex_intro [2: @gget_gt normalize /2 width=1 by/ | skip ] (**) (* explicit constructor *)
]