proposition: Lemma un_i63_bound (x : i63) : (to_Z x < max_int 63)%Z.
proof: Proof. unfold to_Z. case_eq (φ (un_i63 x)%int63 <? max_int 63)%Z; intros equ; try rewrite equ in *. + now apply Zlt_is_lt_bool. + apply Z.ltb_ge in equ. assert (max_int 63 < max_uint 63)%Z by now intros. assert (0 < max_int 63)%Z by now intros. assert ((φ (un_i63 x))%int63 <= (φ Int63.max_int)%int63)%Z. { assert (((φ (un_i63 x))%int63 <= (φ (Int63.max_int))%int63)%Z <-> Int63.leb (un_i63 x) (Int63.max_int) = true). apply Bool.reflect_iff. apply lebP. apply H1. apply int_max_int. } assert ((φ Int63.max_int)%int63 < max_uint 63)%Z by now intros. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)