How to prove that a language is context-free?
A practical approach that in many examples works [but not always, I know] is trying to find the nesting structure of the strings in the language. &quot;Nested dependencies&quot; have to be generated at the same time in different parts of the string.
Also we have the basic toolbox:

concatenation: $S\to S_1S_2$ if you can split the language in two consecutive parts use this production

union: $S\to S_1 \mid S_2$ split into disjoint parts

iteration: $S\to S_1S \mid \varepsilon$


Example 1
Unequal numbers can be handled using a simple trick.
$L= \{ a^mb^n \mid m\neq n \}$
Now clearly
$L= \{ a^mb^n \mid m&lt; n \} \cup  \{ a^mb^n \mid m&gt; n \}$.
Consider first half: $L_1 = \{ a^mb^n \mid m&lt; n \}$. If there must be more $b$'s we can generate an equal numbers of $a$'s and $b$'s on the one and and add at least one extra $b$:
$L_1 = \{ a^mb^m b^i \mid m\ge 0, i&gt;0 \} = \{ a^mb^m \mid m\ge 0 \}\cdot \{ b^i \mid i&gt;0\}$. This we can handle with concatenation from the basic toolbox.
Now the complete language also deal with the case we have more $a$'s. This we handle by using union.
$S \to S_1 \mid S_2$ (choose which part)
$S_1 \to XB$ (extra $b$ part)
$X\to aXb\mid \varepsilon$ (equal number of $a$ and $b$)
$B \to Bb \mid b$ (one or more $b$'s)
$S_2 \to AX$ (extra $a$ part)
$A \to Aa \mid a$ (one or more $a$'s)
Example 2
Here an example for the nesting (thank you Raphael).
$L=\{b^ka^l(bc)^ma^nb^o \mid k,l,m,n,o\in {\Bbb N},k\neq o,2l=n,m\ge 2 \}$
Replace $n$ by $2l$. We can now drop $n$ in conditions.
Replace $k \neq o$ by $k &gt; o \text{ or } k &lt; o$ (confused? $o$ is 'oh' not 'zero'). Apply tools for union. We work with $k &gt; o$ here. Also $k&gt;o$ iff $k=s+o$ and $s&gt;0$ where $s$ is a new variable. Replace $k$ by $s+o$.
$L_1 =\{b^{s+o}a^l(bc)^ma^{2l}b^o \mid l,m,o,s\in {\Bbb N},s&gt;0,m\ge 2 \}$
Some simple rewrites.
$L_1 =\{bb^sb^o a^l bcbc(bc)^m (aa)^{l}b^o \mid l,m,o,s\in {\Bbb N}  \}$
Now we see the nesting structure, and start building a grammar.
$S_1 \to TV$, $T\to bU$, $U\to bU \mid \varepsilon$ (see: concatenation and iteration here)
$V \to bVb \mid W$ (we generate $o$ $b$'s on both sides)
$W \to aWaa\mid X$
$X\to YZ$, $Y\to bcbc$, $Z\to bcZ\mid \varepsilon$
Example 3
$K =\{ a^kb^lc^m \mid l=m+k\}$
A first &quot;obvious&quot; rewrite.
$K =\{ a^kb^{m+k}c^m \mid m,k\ge 0\} = \{ a^kb^mb^kc^m \mid m,k\ge 0\}$
In linguistice this is called &quot;cross-serial dependency&quot;: the interleaving $k,m,k,m$ (usually) strongly indicates non-contextfreeness. Of course $m+k=k+m$ and we are saved.
$K =\{ a^kb^{k+m}c^m \mid m,k\ge 0\} = \{ a^kb^kb^mc^m \mid m,k\ge 0\}$
with productions $S\to XY$, $X\to aXb\mid \varepsilon$, $Y\to bYc\mid \varepsilon$
Similarly $K'= \{ a^kb^lc^m \mid m=k+l\} = \{ a^kb^lc^lc^k \mid k,l\ge 0\}$
with productions $S\to aSc \mid X$, $X\to bXc\mid \varepsilon$

Final comment: these techniques help you come up with a candidate context-free grammar that will hopefully recognize your language.  A correctness proof may still be needed, to ensure that the grammar really works to recognize your language (nothing more, and nothing less).