proposition: Lemma LexProd_Gt_morph : forall x1 x2 : pair, eqPair x1 x2 -> forall x3 x4 : pair, eqPair x3 x4 -> x1 >lex x3 -> x2 >lex x4.
proof: Proof. intros. apply (proj1 (LexProd_Gt_morph_equiv H H0)). hyp. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)