fact: Definition ww_tail0 x := match x with | W0 => ww_zdigits | WW xh xl => match w_compare w_0 xl with | Eq => w_add w_zdigits (w_tail0 xh) | _ => w_0W (w_tail0 xl) end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase