proposition: Lemma i63_mul_assoc (x y z : i63) : x * (y * z) = (x * y) * z.
proof: Proof. apply i63eq_eqb_true_equiv. unfold i63eqb. cbn. generalize (un_i63 x) (un_i63 y) (un_i63 z). clear x y z. intros a b c. assert (((φ (a * (b * c)))%int63 = (φ (a * b * c))%int63)%Z <-> Int63.eqb (a * (b * c))%int63 (a * b * c)%int63 = true). apply Bool.reflect_iff. apply eqbP. apply H. repeat rewrite mul_spec. rewrite (Z.mul_comm (((φ a)%int63 * (φ b)%int63) mod wB) _). repeat rewrite Zmult_mod_idemp_r. rewrite (Z.mul_comm (φ c)%int63 _). now rewrite Z.mul_assoc. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)