proposition: Lemma i63add_assoc (x y z : i63) : x + (y + z) = (x + y) + z.
proof: Proof. unfold i63add, ibinop. apply i63eq_eqb_true_equiv. cbn. rewrite add_assoc. apply eqb_refl. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)