proposition: Lemma i63add_neutral (x : i63): 0 + x = x.
proof: Proof. apply i63eq_eqb_true_equiv. unfold i63eqb. cbn. assert (((φ (0 + un_i63 x))%int63 = (φ (un_i63 x))%int63)%Z <-> Int63.eqb (Int63.add 0 (un_i63 x)) (un_i63 x) = true). apply Bool.reflect_iff. apply eqbP. apply H. rewrite add_spec. change ((φ 0)%int63 + (φ (un_i63 x))%int63)%Z with (φ (un_i63 x))%int63. apply Zmod_small. apply to_Z_bounded. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)