fact: Definition ww_sqrt x := if (ww_is_zero x) then W0 else let p := ww_head1 x in match ww_compare p W0 with | Gt => match ww_add_mul_div p x W0 with W0 => W0 | WW x1 x2 => let (r, _) := w_sqrt2 x1 x2 in WW w_0 (w_add_mul_div (w_sub w_zdigits (low (ww_add_mul_div (ww_pred ww_zdigits) W0 p))) w_0 r) end | _ => match x with W0 => W0 | WW x1 x2 => WW w_0 (fst (w_sqrt2 x1 x2)) end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase