fact: Definition ww_div21 a1 a2 b := match a1 with | W0 => match ww_compare a2 b with | Gt => (ww_1, ww_sub a2 b) | Eq => (ww_1, W0) | Lt => (W0, a2) end | WW a1h a1l => match a2 with | W0 => match b with | W0 => (W0,W0) | WW b1 b2 => let (q1, r) := w_div32 a1h a1l w_0 b1 b2 in match r with | W0 => (WW q1 w_0, W0) | WW r1 r2 => let (q2, s) := w_div32 r1 r2 w_0 b1 b2 in (WW q1 q2, s) end end | WW a2h a2l => match b with | W0 => (W0,W0) | WW b1 b2 => let (q1, r) := w_div32 a1h a1l a2h b1 b2 in match r with | W0 => (WW q1 w_0, w_0W a2l) | WW r1 r2 => let (q2, s) := w_div32 r1 r2 a2l b1 b2 in (WW q1 q2, s) end end end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub