Ehresmann's theorem over the $p$-adics I am looking for a version of Ehresmann's theorem for analytic manifolds over the $p$-adic numbers $\mathbb{Q}_p$ or, more generally, local fields. I follow the conventions from Serre's book "Lie algebras and Lie groups" concerning analytic manifolds over local fields.
Recall that Ehresmann's theorem states that a proper submersion between smooth manifolds is a locally trivial fibration.

Does a version of this hold for analytic manifolds over $\mathbb{Q}_p$? Namely, is a proper submersion between analytic manifolds over $\mathbb{Q}_p$ a locally trivial fibration?

 A: It seems to me that the following lines essentially show that the answer is yes. Let $f\colon X\to Y$ be a proper submersion of $p$-adic manifolds, we want to show that $f$ is locally trivial on the target:
every point $y$ has an open neighborhood $V$ such that $f_V\colon f^{-1}(V)\to V$ is isomorphic to the projection $p_2\colon U\times V\to V$
of a product.
By the inverse function theorem, $f$ is locally trivial on the source:
for every point $x\in X$, there exists an open neighborhood $W$ of $x$
such that $f|_W\colon W\to f(W)$ is isomorphic to a product.
Let $y\in Y$ and let us cover the compact manifold $f^{-1}(y)$ by a finite family $(W_i)$ of open subsets 
on which $f$ is isomorphic to a product $U_i\times V_i \to V_i$. 
Let us refine it to a disjoint finite covering, still denoted by the same letter, of the same form.
The union $W=\bigcup W_i$ is an open neighborhood of $f^{-1}(y)$.
Since $f$ is proper, there exists an open neighborhood $V$ of $y$ such that $W$ contains $f^{-1}(V)$. Replacing $V_i$ by $V$, we are reduced to the case $V_i=V$ for all $i$.
It is now visible that $f^{-1}(V)$ is isomorphic to the projection
of the product $U\times V\to V$, where $U$ is defined as the disjoint union of the $U_i$.
