proposition: Lemma LexProd3_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'. constructor 2; trivial. compute; auto. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)