proposition: Lemma list_lt_not_eq : forall (x y : list A), list_lt x y -> x <> y.
proof: Proof. induction x as [ |x xs IHxs]; intros [ |y ys]; simpl; auto. - discriminate. - intros [H1|[H1 H2]]; intros H; inversion H; subst. + now apply (lt_not_eq _ _ H1). + now apply (IHxs _ H2). Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes