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