Cohomology ring of Grassmannians I'm reading a paper called An Additive Basis for the Cohomology of Real Grassmannians, which begins by making the following claim (paraphrasing):

Let $w=1+w_1+ \ldots + w_m$ be the total Stiefel-Whitney class of the canonical $m$-plane bundle over $G_m(\mathbb{R}^{m+n})$ and let $\bar{w}=1+\bar{w_1}+\ldots+ \bar{w_n}$ be its dual. Then $H^\ast G_m (\mathbb{R}^{m+n})$ is the quotient of the polynomial algebra $\mathbb{Z}_2[1,w_1,\ldots,w_m]$ by the ideal $(\bar w_{m+1},\cdots,\bar {w}_{m+n})$ generated by the relation $w\bar{w}=1$.

The reference provided is to Borel's La cohomologie mod 2 de certains espaces homogènes. As the title suggests, this paper is in French, a language with which I am not familiar.
I'm familiar with the fact that the cohomology ring of the infinite Grassmannian $G_m(\mathbb{R}^\infty)$ is freely generated by $w_1,\ldots,w_m$ over $\mathbb{Z}_2$ (as proved in Hatcher's Vector Bundles), but I can't see how to prove this variant. Any help would be much appreciated. Perhaps someone can even translate the proof given in Borel's paper.
 A: I cannot completely answer the question, but I will write down some thoughts.

First of all, I can determine the graded $\mathbb F_2$-vector space structure of $H^*(G_n(\mathbb R^{n+k}))$. Indeed, $G_n(\mathbb R^{n+k})$ has a cellular decomposition in terms of the so-called Schubert cells, i.e., for any sequence $1\le\sigma_1<\cdots<\sigma_n\le n+k$, let
$$e(\sigma):=\{X\in G_n(\mathbb R^{n+k}):\dim(X\cap\mathbb R^{\sigma_i})=i,\dim(X\cap \mathbb R^{\sigma_i-1})=i-1\ (1\le \forall i\le n)\}.$$
Then, $e(\sigma)$ is a cell of dimension $(\sigma_1-1)+\cdots+(\sigma_n-n)$.
With respect to this cellular decomposition, consider the cellular co-chain complex
$$C^0G_n(\mathbb R^\infty)\to C^1G_n(\mathbb R^\infty)\to\cdots,$$
whose homology is $H^*G_n(\mathbb R^\infty)$.
I claim the derivatives are all $0$. Indeed, a priori $H^iG_n(\mathbb R^\infty)$ is a sub-quotient of $C^iG_n(\mathbb R^\infty)$, but they have the same dimension. Thus, for any finite $k$ we also have $C^iG_n(\mathbb R^{n+k})\cong H^iG_n(\mathbb R^{n+k})$.
In particular, $\dim(H^*G_n(\mathbb R^{n+k}))={n+k\choose n}$.

Also from the above argument, we see that the injection $G_n(\mathbb R^{n+k})\hookrightarrow G_n(\mathbb R^\infty)$ induces a surjection on the cellular co-chains, i.e., there is a surjection
$$u\colon H^*G_n(\mathbb R^\infty)=\mathbb F_2[w_1,\cdots,w_n]\to H^*G_n(\mathbb R^{n+k}).$$
Moreover, consider the canonical $n$-dimensional vector bundle $\xi$ on $G_n(\mathbb R^{n+k})$. There is an exact sequence
$$0\to \xi\to\epsilon^{n+k}\to\eta\to 0,$$
where $\epsilon$ is the trivial line bundle, and $\eta$ is a rank $k$ bundle. Here, $\eta$ is the pull-back of the dual of the canonical bundle along $G_n(\mathbb R^{n+k})\cong G_k(\mathbb R^{n+k})\hookrightarrow G_k(\mathbb R^\infty)$, so has Stiefel-Whitney class $1+\overline w_1+\cdots+\overline w_k$. Similarly, $\xi$ is the pull-back of the canonical bundle along $G_n(\mathbb R^{n+k})\hookrightarrow G_n(\mathbb R^\infty)$, so has Stiefel-Whitney class $1+w_1+\cdots+w_n$. Thus, the short exact sequence above tells us
$$\begin{align*}
1&=w(\epsilon^{n+k})\\
&=w(\xi)w(\eta)\\
&=(1+w_1+\cdots+w_n)(1+\overline{w}_1+\cdots+\overline w_k),
\end{align*}$$
so the surjection $u$ factors through:
$$A_{n,k}:=\mathbb F_2[w_1,\dots,w_n]/((1+w_1+\cdots+w_n)(1+\overline{w}_1+\cdots+\overline w_k)-1)\to H^*G_n(\mathbb R^{n+k}).$$
Thus, to prove isomorphism, it suffices to calculate the dimension of the quotient, which should be ${n+k\choose n}$.

One strategy might be to look at the homomorphism $G_n(\mathbb R^{n+k})\hookrightarrow G_n(\mathbb R^{n+k+1})$, given by the injection $\mathbb R^{n+k}\hookrightarrow\mathbb R^{n+k+1}$. This gives a commutative diagram
$\require{AMScd}$
\begin{CD}
A_{n,k+1} @>>> A_{n,k}\\
@VVV @VVV\\
H^*G_n(\mathbb R^{n+k+1}) @>>> H^*G_n(\mathbb R^{n+k}),
\end{CD}
where all maps are surjections. It suffices to somehow put the kernel of $A_{n,k+1}\to A_{n,k}$ into bijection with $A_{n-1,k+1}$ to make the induction run.
