proposition: Lemma prod_lt_not_eq : forall (x y:A*B), prod_lt x y -> x <> y.
proof: Proof. intros [a1 b1] [a2 b2]; simpl. intros [H1|[_ H1]] H3; inversion H3 as [[H4 H5]]; clear H3; subst a2 b2; now apply (lt_not_eq _ _ H1). Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes