proposition: Lemma Vrel1_sub : forall n (v1 v2 : vector A n) p q (h : p+q<=n), Vrel1 R v1 v2 -> (Vrel1 R)% (Vsub v1 h) (Vsub v2 h).
proof: Proof. intros n v1 v2 p q k. rewrite Vrel1_nth_iff. intros [i [hi [i1 i2]]]. destruct (lt_dec i p). left. apply Veq_nth. intros j hj. rewrite !Vnth_sub. apply i2. lia. destruct (ge_dec i (p+q)). left. apply Veq_nth. intros j hj. rewrite !Vnth_sub. apply i2. lia. right. rewrite Vrel1_nth_iff. exists (i-p). assert (l : i-p<q). lia. exists l. split. rewrite !Vnth_sub. erewrite Vnth_eq, Vnth_eq with (v:=v2). apply i1. lia. lia. intros j hj m. rewrite !Vnth_sub. apply i2. lia. Qed.
imports: CoLoR(LogicUtil VecUtil RelUtil NatUtil SN)