proposition: Lemma option_lt_trans : forall (x y z : option A), option_lt x y -> option_lt y z -> option_lt x z.
proof: Proof. intros [a| ] [b| ] [c| ]; simpl; auto. - apply lt_trans. - intros _ []. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes