proposition: Lemma without_c_b: forall w2, [|w2|] < [|b|] -> [|w_succ w2|] = [|w2|] + 1.
proof: Proof. intros w2 H. unfold w_succ;rewrite ZnZ.spec_succ. rewrite Zmod_small;auto. assert (HH := ZnZ.spec_to_Z w2). assert (HH' := ZnZ.spec_to_Z b);auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux