proposition: Lemma decr_correct n : (0 < [n])%Z -> ([n.-1] = [n] - 1)%Z.
proof: Proof. induction n as [ | a n Hrec]; nrom. auto with zarith. unfold decr_num; fold decr_num. case (to_Z_bounded a); nrom; intros Ha1 Ha2. rewrite compare_spec; case Z.compare_spec; nrom; try rewrite spec_Bm1; nrom. 2: auto with zarith. intros H1 H2; rewrite H1 in H2 |- *; rewrite Hrec; auto with zarith; try ring. apply Zmult_lt_0_reg_r with wB; auto with zarith. rewrite Zmult_comm; auto with zarith. intros H1 H2. rewrite sub_spec; nrom. rewrite Zmod_small; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63