fact: Fixpoint alternate (l1 l2 : seq nat) : seq nat := match (l1, l2) with | ([::], ys) => ys | (xs, [::]) => xs | (x::xs, y::ys) => x :: y :: (alternate xs ys) end.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype seq)