proposition: Lemma eqm_mod x y : x mod wB ≡ y mod wB → x ≡ y.
proof: Proof. intros h. eapply (eqm_trans). - apply eqm_sym; apply Zmod_eqm. - apply (eqm_trans _ _ _ _ h). apply Zmod_eqm. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63