proposition: Lemma of_to_Z : forall x, of_Z (to_Z x) = x.
proof: Proof. unfold to_Z, of_Z. intros x. generalize (Uint63.to_Z_bounded x). case ltbP. - intros ltxmin [leq0x _]. generalize (Uint63.of_to_Z x). destruct (φ x%uint63). + now intros <-. + now intros <-; unfold Uint63.of_Z. + now intros _. - intros nltxmin leq0xltwB. rewrite (opp_spec x). rewrite Z_mod_nz_opp_full. + rewrite Zmod_small by easy. destruct (wB - φ x%uint63) eqn: iswbmx. * lia. * simpl. apply to_Z_inj. rewrite opp_spec. generalize (of_Z_spec (Z.pos p)). simpl Uint63.of_Z; intros ->. rewrite <- iswbmx. rewrite <- Z.sub_0_l. rewrite <- (Zmod_0_l wB). rewrite <- Zminus_mod. replace (0 - _) with (φ x%uint63 - wB) by ring. rewrite <- Zminus_mod_idemp_r. rewrite Z_mod_same_full. rewrite Z.sub_0_r. now rewrite Z.mod_small. * lia. + rewrite Z.mod_small by easy. intros eqx0; revert nltxmin; rewrite eqx0. now compute. Qed.
imports: ZArith Uint63 Lia