fact: Axioms (i63sub_max_safe : forall (x : i63) (xpos : 0 <= x), i63sub_safe max_i63 x) (i63add_min_safe : forall (x : i63) (xpos : 0 <= x), i63add_safe min_i63 x) (i63sub_unwrap : forall (x y : i63) (ypos : 0 <= y), min_i63 + y <= x <-> i63sub_safe x y) (i63add_unwrap : forall (x y : i63) (ypos : 0 <= y), x <= max_i63 - y <-> i63add_safe x y) (i63sub_add_cancel : forall (x y : i63), x - y + y = x) (i63add_sub_cancel : forall (x y : i63), x + y - y = x).
imports: Coq(RelationClasses ZArith Int63 Lia)