proposition: Theorem high_zero:forall x, [[x]] < base w_digits -> [|fst (split x)|] = 0.
proof: Proof. intros x; case x; simpl; auto. intros xh xl H; case (Zle_lt_or_eq 0 [|xh|]); auto with zarith. case (ZnZ.spec_to_Z xh); auto with zarith. intros H1; contradict H; apply Zle_not_lt. assert (HHHH := wB_pos w_digits). unfold w_to_Z. match goal with |- ?X <= ?Y + ?Z => pattern X at 1; rewrite <- (Zmult_1_l X); auto with zarith; apply Z.le_trans with Y; auto with zarith end. case (ZnZ.spec_to_Z xl); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux