proposition: Lemma i63add_unwrap_neg (x y : i63) (xneg : x <= 0) (ypos : 0 <= y) : i63add_safe x y.
proof: Proof. apply i63add_unwrap; auto. transitivity 0; auto. unfold i63le in *. rewrite i63sub_max_safe; auto. assert (to_Z y <= to_Z max_i63)%Z by apply i63le_max_int. change (to_Z 0) with 0%Z in *. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)