proposition: Lemma i63sub_safe_pos (x y : i63) (ymin : 0 <= y) (ymax : y <= x) : i63sub_safe x y.
proof: Proof. unfold i63sub_safe. apply i63sub_unwrap. + exact ymin. + assert (min_i63 + max_i63 <= 0) by (intro H; discriminate). assert (x <= max_i63) by auto with i63. unfold i63le in *. rewrite i63add_min_safe; auto. change (to_Z 0) with 0%Z in *. rewrite i63add_min_safe in *; auto with i63. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)