Designing CFG that accepts $b^m a^n$ ($m ≤ n$)

I am trying to design a CFG that generates the language $$\{a^k b^m a^n a^k \mid m \leq n\}$$. However, I am having trouble with the $$b^m a^n$$ where $$m \leq n$$. How do I solve this?

• Think of it as $b^m a^m a^k$ where $k = n-m \ge 0$ – rici Jun 3 '20 at 5:24
• So you know you'll have to generate $P\to bPa$, except sometimes the $b$ might be missing... – frabala Jun 3 '20 at 6:11

You can write this language as $$\{ a^k b^m a^m a^\ell a^k \mid k,m,\ell \in \mathbb{N} \}.$$ This description easily lends itself to conversion into a context-free grammar.