proposition: Lemma _succ_mod_spec: forall w t, [|w|]= t mod [|b|] -> [|_succ_mod w|] = ([|w|] + 1) mod [|b|].
proof: Proof. intros w2 t H; unfold _succ_mod, w_compare; simpl. assert (F: [|w2|] < [|b|]). case (Z_mod_lt t [|b|]); auto with zarith. rewrite ZnZ.spec_compare; case Z.compare_spec; intros H1; match goal with H: context[w_succ _] |- _ => generalize H; clear H; rewrite (without_c_b _ F); intros H1; auto with zarith end. rewrite H1, Z_mod_same, _w0_is_0; auto with zarith. rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z w2); auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux