proposition: Lemma spec_split : forall (n : nat) (x : zn2z (word w n)), let (h, l) := double_split w_0 n x in [!S n | x!] = [!n | h!] * double_wB w_digits n + [!n | l!].
proof: Proof. Proof (spec_double_split w_0 w_digits w_to_Z spec_0). Lemma spec_double_divn1_0 : forall n r a, [|r|] < [|b2p|] -> let (q,r') := double_divn1_0 n r a in [|r|] * double_wB w_digits n + [!n|a!] = [!n|q!] * [|b2p|] + [|r'|] /\ 0 <= [|r'|] < [|b2p|]. Proof. induction n;intros. exact (spec_div21 a b2p_le H). simpl (double_divn1_0 (S n) r a); unfold double_divn1_0_aux. assert (H1 := spec_split n a);destruct (double_split w_0 n a) as (hh,hl). rewrite H1. assert (H2 := IHn r hh H);destruct (double_divn1_0 n r hh) as (qh,rh). destruct H2. assert ([|rh|] < [|b2p|]). lia. assert (H4 := IHn rh hl H3);destruct (double_divn1_0 n rh hl) as (ql,rl). destruct H4;split;trivial. rewrite spec_double_WW;trivial. rewrite <- double_wB_wwB. rewrite Z.mul_assoc;rewrite Z.add_assoc;rewrite <- Z.mul_add_distr_r. rewrite H0;rewrite Z.mul_add_distr_r;rewrite <- Z.add_assoc. rewrite H4;ring. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase