proposition: Lemma Vrel1_nth_iff : forall n (v1 v2 : vector A n), Vrel1 R v1 v2 <-> Vrel1_nth R v1 v2.
proof: Proof. intros n v1 v2. rewrite Vrel1_app_iff. split. intros [i [vi [x [j [vj [h [y [h1 [h2 h3]]]]]]]]]; subst; rewrite !Vcast_refl. exists i. assert (hi : i<i+S j). lia. exists hi. rewrite !Vnth_app_cons. intuition. rewrite !Vnth_app. destruct (le_gt_dec i j0). 2: refl. rewrite !Vnth_cons. destruct (lt_ge_dec 0 (j0-i)). 2: lia. apply Vnth_eq. refl. intros [i [hi [i1 i2]]]. assert (ki : 0+i<=n). lia. ex i (Vsub v1 ki) (Vnth v1 hi). assert (kj : S i+(n-i-1)<=n). lia. ex (n-i-1) (Vsub v1 kj). assert (k : i+S(n-i-1)=n). lia. ex k (Vnth v2 hi). split; [idtac|split;[idtac|hyp]]. apply Veq_nth. intros j hj. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i j). rewrite Vnth_cons. destruct (lt_ge_dec 0 (j-i)). rewrite Vnth_sub. apply Vnth_eq. clear -l0; lia. apply Vnth_eq. clear -l g; lia. rewrite Vnth_sub. apply Vnth_eq. refl. apply Veq_nth. intros j hj. rewrite Vnth_cast, Vnth_app. destruct (le_gt_dec i j). rewrite Vnth_cons. destruct (lt_ge_dec 0 (j-i)). rewrite Vnth_sub. trans (Vnth v1 hj). sym. apply i2. clear -l0; lia. apply Vnth_eq. clear -l0; lia. apply Vnth_eq. clear -l g; lia. rewrite Vnth_sub. trans (Vnth v1 hj). sym. apply i2. clear -g; lia. apply Vnth_eq. refl. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)