Say we walk on a finite, connected, even-degree graph with no self loops in the following way: we start from an arbitrary vertex $s \in V$, at each step choosing an untraversed edge incident to the current vertex, until it gets stuck because there are no more adjacent untraversed edges. I want to prove by induction on the length of the walk that whenever this walk visits a vertex $v \neq s$, it has traversed an odd number of edges incident to $v$, and that whenever it enters $s$ it will have traversed an even number of edges incident to $s$. Proving this will allow us to show that the walk will eventually get stuck at the starting vertex, so this walk produces a tour.
I am aware of why these are the case due to the patterns of how we exit and enter these vertices and can pair up entering and exiting them via distinct edges. However, I am stuck on how to inductively prove this on the length of the walk, because the length of the walk isn't correlated with how many times we enter and exit a vertex. I have started by assuming that for all graphs having the conditions earlier stipulated, every walk of length $k$ or less possesses this property. And then I try to make a walk of length $k+1$ devolve into a smaller walk somehow, but am stuck as far as the formal process. How could we formally prove this?
I am trying to solve this problem to better understand Euler's theorem.