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: CRtrans Compress ARtrans ARbigD ARroot dyadics BigZ