proposition: Lemma i63add_safe_lt_add (x y z : i63) (safe1 : i63add_safe x y) (safe2 : i63add_safe x z) (lt : y < z) : x + y < x + z.
proof: Proof. unfold i63lt in *. rewrite safe1, safe2. lia. Qed.
imports: Coq(RelationClasses ZArith Int63 Lia)