proposition: Lemma eqm_subE x y : x ≡ y ↔ x - y ≡ 0.
proof: Proof. split. - apply eqm_sub. - intros h; case (eqmE _ _ h); clear h; intros q h. assert (y = x - q * wB) by lia. clear h; subst y. unfold eqm; rewrite Zminus_mod, Z_mod_mult, Z.sub_0_r, Zmod_mod; reflexivity. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63