proposition: Lemma ltb_bool_iff_lt: forall x y, ltb_bool x y = true <-> lt_bool x y.
proof: Proof. intros x y; split; intro H; case_eq x; case_eq y; intros; subst; compute in *; easy. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes