proposition: Lemma sub1_cp a b : match (a - (1 + b)) ?= a with | Lt => (to_Z (a - (1 + b)) = to_Z a - (1 + to_Z b))%Z | _ => (to_Z (a - (1 + b)) = to_Z a - (1 + to_Z b) + 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 (1 + b)); nrom; intros H1b1 H1b2. case (to_Z_bounded (a - (1 + b))); nrom; intros Hab1 Hab2. case (Zle_lt_or_eq (1 + to_Z b) wB); auto with zarith; intros Hb3; try( rewrite compare_spec; case Z.compare_spec; intros Hc; auto with zarith; generalize Hc; rewrite sub_spec, add_spec; nrom; rewrite Hb3, Z_mod_same_full, Zminus_0_r, Zmod_small; auto with zarith). assert (H1b: to_Z (1 + b) = (to_Z b + 1)%Z). rewrite add_spec, Zmod_small; nrom; auto with zarith. assert (H1ab: (to_Z a - to_Z (1 + b) < wB)%Z); auto with zarith. case (Zle_or_lt 0 (to_Z a - to_Z (1 + b))); intros Hab. assert (He: (to_Z(a - (1 + b)) = to_Z a - to_Z b - 1)%Z). rewrite sub_spec, Zmod_small; nrom; auto with zarith. rewrite compare_spec; case Z.compare_spec; intros Hc; auto with zarith. assert (He: (to_Z(a - (1 + b)) = to_Z a - to_Z b - 1 + wB)%Z). rewrite <- (fun x y => Zmod_small (x + y) wB); auto with zarith. rewrite Zplus_mod, Z_mod_same_full, Zplus_0_r, Zmod_mod; auto with zarith. rewrite sub_spec, H1b; nrom; apply f_equal2 with (f := Z.modulo); auto with zarith. rewrite compare_spec; case Z.compare_spec; intros Hc; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63