proposition: Lemma lexprod_trans : forall a b c, a >lex b -> b >lex c -> a >lex c.
proof: Proof. intros a b c ab bc; inversion ab as [ la la' lb lb' gt_la lL lR | la la' lb lb' eq_la gt_lb lL lR ]; inversion bc as [ ra ra' rb rb' gt_ra rL rR | ra ra' rb rb' eq_ra gt_rb rL rR ]; assert (eq1: la' = ra); try solve [congruence]; assert (eq2: lb' = rb); try solve [congruence]. constructor 1; apply (sord_trans gtL_so la la' ra'); solve [trivial | rewrite eq1; trivial]. constructor 1. rewrite <- eq_ra, <- eq1. hyp. constructor 1. rewrite eq_la, eq1. hyp. constructor 2. rewrite eq_la, <- eq_ra, eq1. auto with sets. apply (sord_trans gtR_so lb lb' rb'); [ trivial | rewrite eq2; trivial ]. Qed.
imports: CoLoR(LogicUtil RelUtil RelExtras) Coq(Setoid Morphisms Basics)