proposition: Lemma z2Zx1: forall x, z2Z (Z2z x) = z2Z (Z2z x) mod z2Z zN.
proof: Proof. unfold Z2z; intros x. generalize (Z_mod_lt x exx.(vN)). case_eq (x mod exx.(vN)). intros _ _. simpl; unfold z2Z; rewrite ZnZ.spec_0; auto. intros p H1 H2. case (ZnZ.spec_to_Z zN). generalize z2ZN; unfold z2Z; intros HH; rewrite HH. intros _ H0. case H2; auto with zarith; clear H2; intros _ H2. rewrite Zmod_small. reflexivity. set (v := ZnZ.of_pos p). split. case (ZnZ.spec_to_Z (snd v)); auto. generalize H2; rewrite (ZnZ.spec_of_pos p); fold v. case (fst v). simpl; auto. intros p1 H. contradict H0; apply Zle_not_lt. apply Zlt_le_weak; apply Z.le_lt_trans with (2:= H). apply Z.le_trans with (1 * base (ZnZ.digits op) + 0). auto with zarith. apply Zplus_le_compat. apply Zmult_gt_0_le_compat_r. case (ZnZ.spec_to_Z (snd v)); auto with zarith. case p1; red; simpl; intros; discriminate. case (ZnZ.spec_to_Z (snd v)); auto with zarith. intros p Hp; case (Z_mod_lt x exx.(vN)). auto with zarith. rewrite Hp; intros HH; case HH; auto. Qed.
imports: ZArith Znumtheory Zpow_facts CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) W Mod_op ZEll Bits Zmod