fact: Definition ww_add x y := match x, y with | W0, _ => y | _, W0 => x | WW xh xl, WW yh yl => match w_add_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