proposition: Lemma spec_get_low: forall n x, [!n | x!] < wB -> [|get_low n x|] = [!n | x!].
proof: Proof. clear spec_w_1 spec_w_Bm1. intros n; elim n; auto; clear n. intros n Hrec x; case x; clear x; auto. intros xx yy; simpl. destruct (spec_double_to_Z n xx) as [F1 _]. Z.le_elim F1. - intros; exfalso. assert (F3 := double_wB_more_digits n). destruct (spec_double_to_Z n yy) as [F4 _]. assert (F5: 1 * wB <= [!n | xx!] * double_wB n); auto with zarith. apply Z.mul_le_mono_nonneg; auto with zarith. unfold base; auto with zarith. - rewrite <- F1; rewrite Z.mul_0_l, Z.add_0_l. intros; apply Hrec; auto. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType