proposition: Lemma to_Z_mod_Uint63to_Z (x : int) : to_Z x mod wB = φ x%uint63.
proof: Proof. unfold to_Z. case ltbP; [> now rewrite Z.mod_small by now apply Uint63.to_Z_bounded |]. rewrite Z.nlt_ge; intros gexmin. rewrite opp_to_Z_opp; rewrite Z.mod_small by now apply Uint63.to_Z_bounded. - easy. - now intros neqx0; rewrite neqx0 in gexmin. Qed.
imports: ZArith Uint63 Lia