proposition: Lemma incr_correct n : ([n.+1] = [n] + 1)%Z.
proof: Proof. induction n as [ | a n Hrec]; nrom; auto. unfold incr_num; fold incr_num. generalize (add1_cp a); rewrite compare_spec; case Z.compare_spec; nrom; intros HH H; rewrite H; try rewrite Hrec; try ring. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63