fact: Definition w_mul_add x y r := match w_mul_c x y with | W0 => (w_0, r) | WW h l => match w_add_c l r with | C0 lr => (h,lr) | C1 lr => (w_succ h, lr) end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase