fact: Definition ww_add_carry x y := match x, y with | W0, W0 => ww_1 | W0, WW yh yl => ww_succ (WW yh yl) | WW xh xl, W0 => ww_succ (WW xh xl) | WW xh xl, WW yh yl => match w_add_carry_c xl yl with | C0 l => WW (w_add xh yh) l | C1 l => WW (w_add_carry xh yh) l end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase