proposition: Lemma lex_inv_right (a a':A)(b b':B) : ((a,b) <=lex (a',b')) -> a =A= a' -> b <=B b'.
proof: Proof. intros [H|H]. - destruct 1. absurd (a' <A a'). + apply lt_irreflexive. + apply DecPreOrder.le_lt_trans with a;auto. - auto. Qed.
imports: Coq(Arith ZArith List Sets.Finite_sets Sets.Ensembles)