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