proposition: Lemma combine_split_comm : forall A B dim v, let (va,vb) := split_vector A B dim v in (combine_vector A B dim va vb) = v.
proof: Proof. intros A B. induction dim. vm_compute. intros [a b]; simpl; reflexivity. simpl;intros [[a b] v]. simpl. generalize (IHdim v). case (split_vector _ _ dim v). intros;subst;reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)