proposition: Lemma sub_cp a b : match (a - b) ?= a with | Gt => (to_Z (a - b) = to_Z a - to_Z b + 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 (H1ab: (to_Z a - to_Z b < wB)%Z); auto with zarith. case (Zle_or_lt 0 (to_Z a - to_Z b)); intros Hab. assert (He: (to_Z(a - b) = to_Z a - to_Z b)%Z). rewrite sub_spec, Zmod_small; auto with zarith. rewrite compare_spec; case Z.compare_spec; intros Hc; auto with zarith. assert (He: (to_Z(a - b) = to_Z a - to_Z b + 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, <- sub_spec; auto. rewrite compare_spec; case Z.compare_spec; intros Hc; auto with zarith. Qed.
imports: List ZArith Znumtheory Uint63 Cyclic63