proposition: Lemma option_lt_not_eq : forall (x y : option A), option_lt x y -> x <> y.
proof: Proof. intros [a| ] [b| ]; simpl; auto. - intros H1 H2. inversion H2 as [H3]. revert H3. now apply lt_not_eq. - discriminate. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes