fact: Definition BigD_compare (x y : bigD) : comparison := match BigZ.compare (expo x) (expo y) with | Gt => BigZ.compare (BigZ.shiftl (mant x) (expo x - expo y)) (mant y) | _ => BigZ.compare (mant x) (BigZ.shiftl (mant y) (expo y - expo x)) end.
imports: MathClasses.interfaces.abstract_algebra MathClasses.interfaces.integers MathClasses.interfaces.additional_operations MathClasses.implementations.dyadics MathClasses.implementations.fast_integers BigZ