proposition: Lemma lexprod_trans : forall a b c, a >lex b -> b >lex c -> a >lex c.
proof: Proof. unfold LexProd_Gt; intros. eapply lexprod_trans; eauto with sets. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)