fact: Definition BigD_mult (x y : bigD) : bigD := mant x * mant y ▼ expo x + expo y.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.implementations.dyadics MathClasses.implementations.fast_integers BigZ