fact: Definition are_adjacent : pred (seq nat * seq nat)%type := [pred xy | [|| xy.1 == [::] , xy.2 == [::] | (last O xy.1).+1 == head O xy.2]].
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib