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