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