proposition: Lemma prod_lt_trans : forall (x y z:A*B), prod_lt x y -> prod_lt y z -> prod_lt x z.
proof: Proof. intros [a1 b1] [a2 b2] [a3 b3]; simpl. intros [H1|[H1 H4]] [H2|[H2 H3]]. - left. eapply lt_trans; eauto. - subst a3. now left. - subst a2. now left. - subst a2 a3. right. split; auto. eapply lt_trans; eauto. Qed.
imports: Bool OrderedType BinPos ZArith OrderedTypeEx Int63 State BVList FArray SMT_classes