proposition: Lemma add_cp a b : match (a + b) ?= a with | Lt => (to_Z (a + b) = to_Z a + to_Z b - Uint63.wB)%Z | _ => (to_Z (a + b) = to_Z a + to_Z b)%Z end.
proof: Proof. case (to_Z_bounded a); nrom; intros Ha1 Ha2. case (to_Z_bounded b); nrom; intros Hb1 Hb2. case (to_Z_bounded (a + b)); nrom; intros Hab1 Hab2. assert (H2ab: (to_Z a + to_Z b < 2 * Uint63.wB)%Z); auto with zarith. case (Zle_or_lt Uint63.wB (to_Z a + to_Z b)); intros H1ab. assert (He: (to_Z(a + b) = to_Z a + to_Z b - Uint63.wB)%Z). rewrite <- (fun x y => Zmod_small (x - y) Uint63.wB); auto with zarith. rewrite Zminus_mod, Z_mod_same_full, Zminus_0_r, Zmod_mod, <- add_spec; auto. rewrite compare_spec; case Z.compare_spec; nrom; intros Hc; auto with zarith. assert (He: (to_Z(a + b) = to_Z a + to_Z b)%Z). rewrite add_spec, Zmod_small; auto with zarith. rewrite compare_spec; case Z.compare_spec; nrom; intros Hc; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63