proposition: Lemma add_vectors_split n : forall k (v vl vr : vector (vec n) k), (forall i (ip : i < k), Vnth v ip =v Vnth vl ip [+] Vnth vr ip) -> add_vectors v =v add_vectors vl [+] add_vectors vr.
proof: Proof. induction k; intros. VOtac. unfold add_vectors. simpl. rewrite vector_plus_zero_r. refl. VSntac v. VSntac vl. VSntac vr. rewrite !add_vectors_cons, (IHk (Vtail v) (Vtail vl) (Vtail vr)), !Vhead_nth, (H 0 (Nat.lt_0_succ k)). match goal with |- (?A [+] ?B) [+] (?C [+] ?D) =v (?A [+] ?C) [+] (?B [+] ?D) => set (X := A); set (Y := B); set (W := C); set (V := D) end. rewrite <- !vector_plus_assoc, (vector_plus_assoc W Y V), (vector_plus_comm W Y), !vector_plus_assoc. refl. intros. rewrite !Vnth_tail. apply H. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)