proposition: Lemma i63add_safe_pos (x y z : i63) (safe : i63add_safe x z) (ymin : 0 <= y) (ymax : y <= z) : i63add_safe x y.
proof: Proof. assert (zpos : 0 <= z) by now transitivity y. apply i63add_unwrap; auto. apply i63add_unwrap in safe; auto. transitivity (max_i63 - z); auto. unfold i63le in *. repeat rewrite i63sub_max_safe; unfold i63le; auto. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)