proposition: Lemma spec_high : forall n (x:word w n), [|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits).
proof: Proof. induction n;intros. unfold high,double_to_Z. rewrite Pshiftl_nat_0. replace (Zpos w_digits - Zpos w_digits) with 0;try ring. simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith. assert (U2 := spec_double_digits n). assert (U3 : 0 < Zpos w_digits). exact (eq_refl Lt). destruct x;unfold high;fold high. unfold double_to_Z,zn2z_to_Z;rewrite spec_0. rewrite Zdiv_0_l;trivial. assert (U0 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w0); assert (U1 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w1). simpl [!S n|WW w0 w1!]. unfold double_wB,base;rewrite Zdiv_shift_r;auto with zarith. replace (2 ^ (Zpos (w_digits << (S n)) - Zpos w_digits)) with (2^(Zpos (w_digits << n) - Zpos w_digits) * 2^Zpos (w_digits << n)). rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite <- Zpower_exp;auto with zarith. replace (Zpos (w_digits << n) - Zpos w_digits + Zpos (w_digits << n)) with (Zpos (w_digits << (S n)) - Zpos w_digits);trivial. change (Zpos (w_digits << (S n))) with (2*Zpos (w_digits << n));ring. change (Zpos (w_digits << (S n))) with (2*Zpos (w_digits << n)); auto with zarith. Qed.
imports: ZArith Ndigits Lia BigNumPrelude DoubleType DoubleBase