proposition: Lemma lex_strict_intro_right (a a':A)(b b':B) : a =A= a' -> b <B b' -> (a,b) <lex (a',b').
proof: Proof. intros H H1. split. right;auto. now destruct H1. intro H2. absurd (b <B b). apply lt_irreflexive;auto. apply DecPreOrder.lt_le_trans with b';auto. apply (lex_inv_right _ _ _ _ H2). now symmetry. Qed.
imports: Coq(Arith ZArith List Sets.Finite_sets Sets.Ensembles)