proposition: Lemma LexProd3_2 a a' b b' c c' : eqL a a' -> gtM b b' -> (a, b, c) >lex3 (a', b', c').
proof: Proof. intros a_a' b_b'. constructor 1; constructor 2; trivial. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)