fact: Fixpoint Vbreak n1 n2 : vector A (n1+n2) -> vector A n1 * vector A n2 := match n1 with | O => fun v => (Vnil, v) | S p1 => fun v => let w := Vbreak p1 n2 (Vtail v) in (Vcons (Vhead v) (fst w), snd w) end.
imports: Coq(Vector Program Structures.Equalities Morphisms) CoLoR(LogicUtil NatUtil EqUtil ListUtil BoolUtil RelUtil)