fact: Definition option_lt (x y : option A) : Prop := match x, y with | Some a, Some b => lt a b | Some _, None => True | None, Some _ => False | None, None => False end.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes