(*#*
%\begin{convention}\label{convention:div-form}%
- Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy].
(*#*
%\begin{convention}\label{convention:div-form}%
- Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy].