fact: Definition ww_pred_c x := match x with | W0 => C1 ww_Bm1 | WW xh xl => match w_pred_c xl with | C0 l => C0 (w_WW xh l) | C1 _ => match w_pred_c xh with | C0 h => C0 (WW h w_Bm1) | C1 _ => C1 ww_Bm1 end end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase