proposition: Lemma cp_spec i j : CpSpec i j (cp_num i j).
proof: Proof. generalize (cpr_correct i j Eq). unfold cp_num; case Z.compare_spec; intros H1 H2; rewrite H2; constructor; auto. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63