proposition: Lemma opp_to_Z_opp (x : int) : φ x mod wB <> 0 -> (- φ (- x)) mod wB = (φ x) mod wB.
proof: Proof. intros neqx0. rewrite opp_spec. rewrite (Z_mod_nz_opp_full (φ x%uint63)) by assumption. rewrite (Z.mod_small (φ x%uint63)) by apply to_Z_bounded. rewrite <- Z.add_opp_l. rewrite Z.opp_add_distr, Z.opp_involutive. replace (- wB) with (-1 * wB) by easy. rewrite Z_mod_plus by easy. now rewrite Z.mod_small by apply to_Z_bounded. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63