proposition: Lemma _pred_mod_spec: forall w t, [|w|] = t mod [|b|] -> [|_pred_mod w|] = ([|w|] - 1) mod [|b|].
proof: Proof. intros w2 t H; unfold _pred_mod, w_compare, bm1; 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[w2] |- _ => generalize H; clear H; intros H1; autorewrite with w_rewrite; auto with zarith end; try rewrite _w0_is_0; try rewrite _w1_is_1; auto with zarith. rewrite <- H1, _w0_is_0; simpl. rewrite <- (Zmod_plus_one (-1)); auto with zarith. repeat rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z b); auto with zarith. unfold w_pred;rewrite ZnZ.spec_pred; auto. assert (HHH := ZnZ.spec_to_Z b);repeat rewrite Zmod_small;auto with zarith. intros;assert (HHH := 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