fact: Fixpoint double_mul_add_mn1 (m:nat) : word wn m -> w -> w -> w*word wn m := match m return word wn m -> w -> w -> w*word wn m with | O => w_mul_add_n1 | S m1 => let mul_add := double_mul_add_mn1 m1 in fun x y r => match x with | W0 => (w_0,extend wn_0W m1 (extend_n 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 wn_WW m1 h l) end end.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase