Context free grammar for strings with more $a$'s than $b$'s
I would like to prove that the grammar $G$ with the rules $$ S \to SS \mid aSb \mid bSa \mid a \mid \varepsilon $$ generates the language $L = {w \mid \text{$w$ has at least as many $a$'s as $b$'s}}$.
Question
My proof is below, but it feels rather clunky and unintuitive. Does anyone have an alternative proof and/or suggestions for how I can improve what I have?
Proof
Step 1. First, we will show that $\mathcal{L}(G) \subseteq L$. This is immediate from the fact that no rule generates more $b$'s than $a$'s. Let $w \in \mathcal{L}(G)$, generated by $G$ via $S = u_1 \Rightarrow \dots \Rightarrow u_n = w$. In each step where a $b$ is added, an $a$ must also be added. Because $w_1$ has an equal number of $a$'s and $b$'s, each subsequent $w_i$ must have at least many $a$'s than $b$'s. Therefore, $w_n \in L$, and so $\mathcal{L}(G) \subseteq L$.
Step 2. Next, we will show that $G$ generates all strings with an equal number of $a$'s and $b$'s. Let $K$ be the set of all such strings. We argue by induction to show that $K \subseteq \mathcal{L}(G)$.
Base step. Let $w \in K$ such that $|w| = 0$. Then $w$ can be generated by $G$ via $S \Rightarrow \varepsilon$.
Inductive step. Suppose $G$ can generate any string in $K$ length less than or equal to $n$. Let $w \in K$ such that $|w| = n + 1$. We distinguish several cases:
1. $w = aub$ for some string $u$. Because $w$ has an equal number of $a$'s and $b$'s, $u$ must also have an equal number of $a$'s and $b$'s. This implies $u \in K$, and by the inductive hypothesis, $S \Rightarrow^ u$. 330
Thus, $w$ is generated by $G$ via $S \Rightarrow aSb \Rightarrow^ aub$.
2. $w = bua$ for some string $u$. This is the same as the previous case.
3. $w$ starts and ends with $a$. But because $w$ has the same number of $a$'s and $b$'s, there must be a point where the number of $b$'s “catches up” with the number of $a$'s. This implies $w = uv$, where $u, v \in K$ are non-empty. By the inductive hypothesis, $S \Rightarrow^ u$ and $S \Rightarrow^ v$. Thus, $w$ is generated by $G$ via $S \Rightarrow SS \Rightarrow^ uS \Rightarrow^ uv$.
By induction, we conclude that $K \subseteq \mathcal{L}(G)$.
Step 3. Finally, we will show that $L \subseteq \mathcal{L}(G)$. Let $w \in L$. Consider the first occurrence of $b$ in $w$. I claim that this occurrence of $b$ must be contained in some substring of $w$ that has an equal number of $a$'s and $b$'s. To see this, we consider several cases:
1. $w$ starts with $a$. Then there is an $a$ to the left of $w$, so $ab$ is a substring of $w$ that contains the first occurrence of $b$.
2. $w$ starts with $b$. Because $w$ has at least as many $a$'s as $b$'s, there must be some prefix of $w$ that has an equal number of $a$'s and $b$'s.
Identify the largest possible substring and call it $v_1$. Note that $v_1 \in K$. Then $w = u_1v_1x$, where $u_1$ consists solely of $a$'s. 532