fact: Definition prod_lt (x y:A*B) : Prop := let (a1, b1) := x in let (a2, b2) := y in (lt a1 a2) \/ ((a1 = a2) /\ (lt b1 b2)).
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes