fact: Definition mul (x y: t): t := match x, y with | Qz zx, Qz zy => Qz (ZZ.mul zx zy) | Qz zx, Qq ny dy => Qq (ZZ.mul zx ny) dy | Qq nx dx, Qz zy => Qq (ZZ.mul nx zy) dx | Qq nx dx, Qq ny dy => Qq (ZZ.mul nx ny) (NN.mul dx dy) end.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig