proposition: Lemma LexProd3_Gt_inv a b c a' b' c' : (a, b, c) >lex3 (a', b', c') -> gtL a a' \/ (eqL a a' /\ gtM b b') \/ (eqL a a' /\ eqM b b' /\ gtR c c').
proof: Proof. intro ord. inversion_clear ord; inversion_clear H; auto. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)