fact: Fixpoint double_mul_add_n1 (n:nat) : word w n -> w -> w -> w * word w n := match n return word w n -> w -> w -> w * word w n with | O => w_mul_add | S n1 => let mul_add := double_mul_add_n1 n1 in fun x y r => match x with | W0 => (w_0,extend w_0W n1 r) | WW xh xl => let (rl,l) := mul_add xl y r in let (rh,h) := mul_add xh y rl in (rh, double_WW w_WW n1 h l) end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase