proposition: Lemma lex_strict_intro_left (a a':A)(b b':B) : a <A a' -> (a,b) <lex (a',b').
proof: Proof. split. now constructor. intro H0. apply (@lt_irreflexive _ _ PA a). apply DecPreOrder.lt_le_trans with a'; auto. apply (lex_inv_left _ _ _ _ H0). Qed.
imports: Coq(Arith ZArith List Sets.Finite_sets Sets.Ensembles)