proposition: Lemma add_assoc x y z: (x + (y + z) = (x + y) + z)%uint63.
proof: Proof. apply to_Z_inj; rewrite !add_spec. rewrite -> Zplus_mod_idemp_l, Zplus_mod_idemp_r, Zplus_assoc; auto. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63