proposition: Lemma of_Z_spec n : φ (of_Z n) = n mod wB.
proof: Proof. destruct n. - reflexivity. - now simpl; unfold of_pos; rewrite of_pos_rec_spec by lia. - simpl; unfold of_pos; rewrite opp_spec. rewrite of_pos_rec_spec; [ |auto]; fold wB. now rewrite <-(Z.sub_0_l), Zminus_mod_idemp_r. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63