proposition: Lemma add_cancel_l x y z : (x + y = x + z)%uint63 -> y = z.
proof: Proof. intros h; apply int_eqm in h; rewrite !add_spec in h; apply eqm_mod, eqm_sub in h. replace (_ + _ - _) with (φ(y) - φ(z)) in h by lia. rewrite <- eqm_subE in h. apply eqmI, h. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63