proposition: Lemma LexProd3_lt_3 a a' b b' c c' : eqL a' a -> eqM b' b -> gtR c' c -> (a, b, c) <lex3 (a', b', c').
proof: Proof. intros a_a' b_b' c_c'. apply LexProd3_lt. apply LexProd3_3; trivial. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)