proposition: Lemma spec_w_mul_add : forall x y r, let (h,l):= w_mul_add x y r in [|h|]*wB+[|l|] = [|x|]*[|y|] + [|r|].
proof: Proof. assert (fake_use := w_1); clear fake_use. intros x y r;unfold w_mul_add;assert (H:=spec_w_mul_c x y); destruct (w_mul_c x y) as [ |h l];simpl;rewrite <- H. rewrite spec_w_0;trivial. assert (U:=spec_w_add_c l r);destruct (w_add_c l r) as [lr|lr];unfold interp_carry in U;try rewrite Z.mul_1_l in H;simpl. rewrite U;ring. rewrite spec_w_succ. rewrite Zmod_small. rewrite <- Z.add_assoc;rewrite <- U;ring. simpl in H;assert (H1:= Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)). rewrite <- H in H1. assert (H2:=spec_to_Z h);split;zarith. case H1;clear H1;intro H1;clear H1. replace (wB ^ 2 - 2 * wB) with ((wB - 2)*wB). 2:ring. intros H0;assert (U1:= wB_pos w_digits). assert (H1 := beta_lex _ _ _ _ _ H0 (spec_to_Z l));zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase