proposition: Lemma trans_lexico2 : forall A1 A2 (R1:binary A1) (R2:binary A2), trans R1 -> trans R2 -> trans (lexico2 R1 R2).
proof: Proof. Proof using. introv Tr1 Tr2. intros [x1 x2] [y1 y2] [z1 z2] Rxy Ryz. simpls. destruct Rxy as [L1|[Eq1 L1]]; destruct Ryz as [M2|[Eq2 M2]]; subst*. Qed.
imports: TLC(LibTactics LibLogic LibBool LibLogic LibProd LibSum)