proposition: Lemma i63mul_comm (x y : i63) : x * y = y * x.
proof: Proof. apply i63eq_eqb_true_equiv. unfold i63eqb. cbn. generalize (un_i63 x) (un_i63 y). clear x y; intros x y. assert ((φ (x * y)%int63 = (φ (y * x))%int63)%Z <-> Int63.eqb (Int63.mul x y) (Int63.mul y x) = true). apply Bool.reflect_iff. apply eqbP. apply H. repeat rewrite mul_spec. now rewrite Z.mul_comm. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)