I'm pretty sure this is a trivial question but eh...
The Frog Puzzle is a famous 8th-grade problem (playable here):
$3$ red frogs and $3$ blue frogs are sitting on lily pads, with a spare lily pad in between them.
Frogs can slide onto adjacent lily pads or jump over a frog; frogs can't jump over more than one frog. Frogs can't move backwards. Can we swap the red frogs with the blue frogs?
It's fairly easy to solve, even for $n$ red frogs and $m$ blue frogs. But I find it very hard to "mathematize" it : should we see the "pond" as an element of $(\mathbb{Z}_3)^7$ ? Then how can we describe the possible moves ?
Unable to translate this into familiar mathematical terms, I'm thereby very puzzled by this... puzzle. In particular, I can't seem to find why is there always a solution, and only one (up to symetry of course), for any number of frogs. I've tried to make it work in Scylab but I'm very rusty in programmation...
All I've managed to prove is that a frog can't jump over a frog of the same color but I'm not sure this will lead somewhere.
Bonus question : is the number of solution equal to the number of empty lily pads?

I have been unable to come up with anything resembling a formal proof, but I have noticed several things that may help someone do so.
Therefore, let $a$ denote moving the only moveable frog of color $A$ (moving to the right), and let $b$ denote moving the only moveable frog of color $B$ (moving to the left).
If, at any point, two frogs of the same color are in adjacent positions, there is a frog of the other color ahead of them, and the open lilypad is behind them, you have lost.
Using this, it's impossible to ever move $aa$ (if there is a $B$ frog to the right), unless one of the $A$ frogs jumps a $B$ frog.
Extending this, if you have moved $k$ of your $A$-colored frogs, there are at most $k$ jumps possible for the $B$ frogs, and you cannot make more than $(k+1)$ $b$-type moves consecutively.
Stepping through the game case by case, it's pretty easy to manually show that there's one possible choice for the next sequence of moves. (I have no proof for this, but I have not yet found a counterexample).
You get the idea by now, but it shouldn't be too difficult to write an automated prover for small $m$ and $n$.