proposition: Lemma to_Z_bounded : forall x, (to_Z min_int <= to_Z x <= to_Z max_int)%Z.
proof: Proof. intros x; unfold to_Z. case ltbP; [> lia | intros _]. case (ltbP max_int); [> intros _ | now intros H; exfalso; apply H]. rewrite opp_spec. rewrite Z_mod_nz_opp_full by easy. rewrite Z.mod_small by apply Uint63.to_Z_bounded. case ltbP. - intros ltxmin; split. + now transitivity 0%Z; [>| now apply Uint63.to_Z_bounded]. + replace (φ min_int%uint63) with (φ max_int%uint63 + 1)%Z in ltxmin. * lia. * now compute. - rewrite Z.nlt_ge; intros leminx. rewrite opp_spec. rewrite Z_mod_nz_opp_full. + rewrite Z.mod_small by apply Uint63.to_Z_bounded. split. * rewrite <- Z.opp_le_mono. now rewrite <- Z.sub_le_mono_l. * transitivity 0%Z; [>| now apply Uint63.to_Z_bounded]. rewrite Z.opp_nonpos_nonneg. apply Zle_minus_le_0. apply Z.lt_le_incl. now apply Uint63.to_Z_bounded. + rewrite Z.mod_small by apply Uint63.to_Z_bounded. now intros eqx0; rewrite eqx0 in leminx. Qed.
imports: ZArith Uint63 Lia