fact: Definition ww_pos_mod p x := let zdigits := w_0W w_zdigits in match x with | W0 => W0 | WW xh xl => match ww_compare p zdigits with | Eq => w_WW w_0 xl | Lt => w_WW w_0 (w_pos_mod (low p) xl) | Gt => match ww_compare p ww_zdigits with | Lt => let n := low (ww_sub p zdigits) in w_WW (w_pos_mod n xh) xl | _ => x end end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub