proposition: Lemma lexv_trans n : Transitive eq -> Transitive gt -> gt @ eq << gt -> eq @ gt << gt -> Transitive (lexv (n:=n) eq gt).
proof: Proof. intros eq_trans gt_trans gt_eq_r gt_eq_l ts us vs. rewrite !lexv_eq. intros [i [i1 [i2 i3]]] [j [j1 [j2 j3]]]. destruct (lt_dec i j). ex i i1. split. apply gt_eq_r. exists (Vnth us i1). fo. intros k ki kn. trans (Vnth us kn). fo. apply j3. lia. destruct (eq_nat_dec i j). subst j. ex i i1. split. trans (Vnth us i1). hyp. rewrite !(Vnth_eq _ i1 j1); auto. intros k ki kn. trans (Vnth us kn); fo. ex j j1. split. apply gt_eq_l. exists (Vnth us j1). split. firstorder auto with zarith. hyp. intros k kj kn. trans (Vnth us kn). apply i3. lia. fo. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)