proposition: Lemma add1_cp a : match (1 + a) ?= 0 with | Eq => (to_Z a = Uint63.wB - 1)%Z | _ => (to_Z (1 + a) = 1 + to_Z a)%Z end.
proof: Proof. case (to_Z_bounded a); case (to_Z_bounded (1 + a)); generalize (add_cp 1 a); rewrite compare_spec; case Z.compare_spec; rewrite compare_spec; case Z.compare_spec; nrom; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63