fact: Definition ww_square_c x := match x with | W0 => W0 | WW xh xl => let hh := w_square_c xh in let ll := w_square_c xl in let xhxl := w_mul_c xh xl in let (wc,cc) := match ww_add_c xhxl xhxl with | C0 cc => (w_0, cc) | C1 cc => (w_1, cc) end in match cc with | W0 => WW (ww_add hh (w_W0 wc)) ll | WW cch ccl => match ww_add_c (w_W0 ccl) ll with | C0 l => WW (ww_add hh (w_WW wc cch)) l | C1 l => WW (ww_add_carry hh (w_WW wc cch)) l end end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase