proposition: Lemma i63lt_le_pred (x y : i63) : x < y -> x <= y - 1.
proof: Proof. intros equ. assert (i63sub_safe y 1). { apply i63sub_unwrap. + intros F; discriminate. + unfold i63le, i63lt in *. rewrite i63add_min_safe. ++ assert (to_Z min_i63 <= to_Z x)%Z by apply i63le_min_int. change (to_Z 1) with 1%Z. lia. ++ intro F; discriminate. } unfold i63le, i63lt in *. rewrite H. change (to_Z 1) with 1%Z. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)