proposition: Lemma add2_cp a b : match (1 + (a + b)) ?= a with | Gt => (to_Z (1 + (a + b)) = to_Z a + to_Z b + 1)%Z | _ => (to_Z (1 + (a + b)) = to_Z a + to_Z b + 1 - Uint63.wB)%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. case (to_Z_bounded (1 + (a + b))); nrom; intros H1ab1 H1ab2. generalize (add_cp 1 (a + b)) (add_cp a b); do 2 (rewrite compare_spec; case Z.compare_spec); nrom; intros H1 H2; lazy zeta; rewrite compare_spec; case Z.compare_spec; nrom; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63