proposition: Lemma spec_double_mul_add_n1 : forall n x y r, let (h,l) := double_mul_add_n1 w_mul_add n x y r in [|h|]*double_wB w_digits n + [!n|l!] = [!n|x!]*[|y|]+[|r|].
proof: Proof. induction n;intros x y r;trivial. exact (spec_w_mul_add x y r). unfold double_mul_add_n1;destruct x as[ |xh xl]; fold(double_mul_add_n1 w_mul_add). rewrite spec_w_0;rewrite spec_extend;simpl;trivial. assert(H:=IHn xl y r);destruct (double_mul_add_n1 w_mul_add n xl y r)as(rl,l). assert(U:=IHn xh y rl);destruct(double_mul_add_n1 w_mul_add n xh y rl)as(rh,h). rewrite <- double_wB_wwB. rewrite spec_double_WW;simpl;trivial. rewrite Z.mul_add_distr_r;rewrite <- Z.add_assoc;rewrite <- H. rewrite Z.mul_assoc;rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite U;ring. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase