let expt n i = let rec loop = function | 0 -> mk_singleton Q.one | n -> mult i (loop (n - 1)) in let j = loop n in if n mod 2 = 0 then inter j mk_nonneg else j