proposition: Lemma lex_of_equiv (a a':A)(b b':B) : a =A= a' -> b =B= b' -> preorder_equiv (a,b) (a',b').
proof: Proof. intros H1 H2; destruct H1, H2;split; right;auto; split;auto. Qed.
imports: Coq(Arith ZArith List Sets.Finite_sets Sets.Ensembles)