proposition: Lemma zerop_correct n : if zerop_num n then [n] = 0%Z else [n] <> 0%Z.
proof: Proof. induction n as [ | a n Hrec]. simpl; auto. case (to_Z_bounded a); nrom; intros Ha1 Ha2. unfold zerop_num; fold zerop_num. rewrite compare_spec; case Z.compare_spec; nrom. 2: auto with zarith. generalize Hrec; case zerop_num. intros H1 H2; rewrite H1, H2; ring. intros H1 H2; rewrite H2. rewrite Zplus_0_l; intros HH; case (Zmult_integral _ _ HH); auto with zarith. generalize (to_Z_pos n); intros H1 H2 H3. enough (0 < to_Z a + wB * [n])%Z by auto with zarith. apply Z.lt_le_trans with (to_Z a). auto with zarith. assert (0 <= wB * [n])%Z; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63