proposition: Lemma i63mul_neutral (x : i63) : 1 * x = x.
proof: Proof. apply i63eq_eqb_true_equiv. unfold i63eqb. cbn. assert (((φ (1 * un_i63 x))%int63 = (φ (un_i63 x))%int63)%Z <-> Int63.eqb (Int63.mul 1 (un_i63 x)) (un_i63 x) = true). apply Bool.reflect_iff. apply eqbP. apply H. rewrite mul_spec. change (φ (1)%int63) with 1%Z. rewrite Z.mul_1_l. apply Zmod_small. apply to_Z_bounded. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)