fact: Definition double_divn1_0_aux n (divn1: w -> word w n -> word w n * w) r h := let (hh,hl) := double_split w_0 n h in let (qh,rh) := divn1 r hh in let (ql,rl) := divn1 rh hl in (double_WW w_WW n qh ql, rl).
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase