proposition: Lemma LexProd3_1 a a' b b' c c' : gtL a a' -> (a, b, c) >lex3 (a', b', c').
proof: Proof. intro a_a'. constructor 1; constructor 1; trivial. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)