proposition: Lemma i63add_safe_le (x y : i63) (safe : i63add_safe x y) (ypos : 0 <= y) : x <= x + y.
proof: Proof. unfold i63lt, i63le in *. rewrite safe. change (to_Z 0) with 0%Z in ypos. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)