proposition: Lemma lexv_opt_filter_sorted_mon_arg A (eq gt : relation A) n (ks : vector nat n) (ks_sorted : sorted ks) p (ts : vector A p) q (us : vector A q) p' (ts' : vector A p') q' (us' : vector A q') : lexv (opt eq) (opt gt) (Vopt_filter ks ts) (Vopt_filter ks us) -> lexv (opt eq) (opt gt) (Vopt_filter ks (Vapp ts ts')) (Vopt_filter ks (Vapp us us')).
proof: Proof. rewrite !lexv_eq. intros [i [i1 [i2 i3]]]. ex i i1. split. revert i2. rewrite !Vnth_opt_filter. destruct (lt_dec (Vnth ks i1) p); destruct (lt_dec (Vnth ks i1) q); destruct (lt_dec (Vnth ks i1) (p+p')); destruct (lt_dec (Vnth ks i1) (q+q')); try (refl || (exfalso; lia) || by (intro h; inversion h)). rewrite !Vnth_app. destruct (le_gt_dec p (Vnth ks i1)); destruct (le_gt_dec q (Vnth ks i1)); try (refl || (exfalso; lia) || by (intro h; inversion h)). rewrite Vnth_eq with (h1:=l) (h2:=g), Vnth_eq with (h1:=l0) (h2:=g0); auto. intros j ji hj. gen (i3 _ ji hj). rewrite !Vnth_opt_filter. destruct (lt_dec (Vnth ks hj) p); destruct (lt_dec (Vnth ks hj) q); destruct (lt_dec (Vnth ks hj) (p+p')); destruct (lt_dec (Vnth ks hj) (q+q')); try (refl || (exfalso; lia) || by (intro h; inversion h)). rewrite !Vnth_app. destruct (le_gt_dec p (Vnth ks hj)); destruct (le_gt_dec q (Vnth ks hj)); try (refl || (exfalso; lia) || by (intro h; inversion h)). rewrite Vnth_eq with (h1:=l) (h2:=g), Vnth_eq with (h1:=l0) (h2:=g0); auto. Qed.
imports: Coq(Morphisms Basics) CoLoR(SN LogicUtil NatUtil VecUtil VecOrd ListUtil RelUtil)