Examples of bi-implications ($\Leftrightarrow$) where the $\Rightarrow$ direction is used in the proof of the $\Leftarrow$ direction. [I'm asking for examples of proofs with a certain structure. There is quite a lot of text before arriving at the questions. This is because asking for examples of a phenomenon is best carried out by giving more examples of said phenomenon. Do however feel free to skip ahead to the questions if you think you get it]
Here are three cute theorems that don't seem to have much in common (but wait and see!). I write the proofs a bit sketchily because they have no relevance for the question, except in that we want to establish that all three theorems have 'direct' proofs that don't depend on the things to come.
Thm. 1 (Pythagoras): The lengths $a, b, c$ of the sides of a right angled triangle satisfy $a^2 + b^2 = c^2.$
Proof: Visit your local library.
Thm. 2 (Thales): Let $A$, $B$ be anti-podal points on a circle $c$ (so segment $AB$ is a diameter of $c$.) Let $C$ be any other point on $c$. Then the triangle $ABC$ has a right angle at C.
Proof: Find the center $M$ of $c$ (so $M$ is the midpoint of $AB$) and draw the segment $MC$. By the definition of circle, the two new triangles we created are isosceles and so each has a pair of equal angles (on the circle). Now apply the fact that the sum of the angles in a triangle equals 180 degrees. (This argument is much clearer when you actually draw the picture.)
Thm. 3 (Mersenne): Let $m, n$ be positive integers such that $m$ is a divisor of $n$. Then $2^m - 1$ is a divisor of $2^n - 1$.
Proof: With pleasure I quote an extremely slick proof by MSE user @René: in binary $2^m - 1$ is written $111 \cdots 1$ ($m$ ones) and $2^n-1$ is written $111111 \cdots 11$ ($n$ ones). Now if $m$ divides $n$ it is easy to see that we can get from $2^m -1$ to $2^n -1$ by multiplying with $100 \cdots 010 \cdots 010 \cdots 01$.
Now what do these theorems have in common? At least three things that I call a) b) and c) below. (The first two are manifestly unspectacular so please bear with me until point c).)
a) All three theorems are of the form: if an object $x$ of type $X$ has property $Y$, it necessarily also has property $Z$.
b) In all three cases the converse 'if object $x$ of type $X$ has property $Z$, it necessarily also has property $Y$' is also true.
Concretely we have:
Thm. 1': (Reverse Pythagoras): If the side lengths $a, b, c$ of a triangle satisfy $a^2 + b^2 = c^2$ then the triangle has a right angle.
Thm. 2': (Reverse Thales): If triangle $ABC$ has a right angle at $C$ the then $C$ lies on the circle of which $AB$ is a diameter.
Thm. 3': (Reverse Mersenne): If $m, n$ are positive integers such that $2^m -1$ divides $2^n-1$ then $m$ divides $n$.
c) Thms 1', 2', 3' have essentially the same proof! (well, proof structure).
In particular all three proofs use the ordinary, non-reversed version (i.e. thm 1, 2 or 3) of the theorem (1', 2', 3')  they want to prove, as well as what I like to call a 'this town ain't big enough for the two of us'-argument. I spell this out in all three cases below, before moving to the questions, writing the common structure in block-brackets.
Proof of theorem 1':
[Step 0, let an object x of type X with property Z be given. We want to show that it has property Y:] Let $ABC$ be a triangle satisfying $a^2 + b^2 = c^2$ where we use the standard notation $|BC| =a$, $|CA| = b$, $|AB| = c$. We want to show that $\angle C = 90^\circ$.
[Step 1, construct an object $x'$ that is 'close' to $x$ but already has property $Y$:] Consider a triangle A'B'C' such that $|A'C'| = b$, $\angle C = 90^\circ$ and $|C'B'| = a$. (For dramatic visual effect we may assume that $A' = A$ and rotate the new triangle such that $A'B'$ lies on the same line as $AB$, though that is not strictly necessary.)
[Step 2, by the non-reversed version of the theorem, object $x'$ also has property $Z$:] By Pythagoras theorem, the hypotenuse $A'B'$ of the new triangle has length $c$, that is, the same length as the hypotenuse $AB$ of the old triangle.
[Step 3, this town ain't big enough for two objects with property $Z$:]
It is clear that we can't have two different triangles with side lengths $a, b$ and $c$. Hence $A'B'C'$ is congruent (or if we place it as described in parentheses in step 1 equal) to $ABC$.
[Step 4: if $x = x'$ then $x$ has all the properties of $x'$, in particular property $Y$.] But $A'B'C'$ had a right angle by definition. If $ABC$ is congruent to it, so does $ABC$.
Proof of theorem 2':
[Step 0, let an object x of type X with property Z be given. We want to show that it has property Y:] Let a triangle ABC be given and assume that $\angle C = 90^\circ$. We want to show that $C$ lies on the circle of which $AB$ is a diameter. Since we are talking about this circle we might as well draw it  and call it $c$.
[Step 1, construct an object $x'$ that is 'close' to $x$ but already has property $Y$:] Let $C'$ be the intersection of $BC$ (after extending it if needed) with circle $c$. The new triangle $ABC'$ is 'close' to triangle $ABC$ in that it shares two points and one angle with it. 
[Step 2, by the non-reversed version of the theorem, object $x'$ also has property $Z$:] Since $C'$ lies on $c$, Thm. 2 states that $\angle BC'A = 90^\circ$.
[Step 3, this town ain't big enough for two objects with property $Z$:] Both $AC$ and $AC'$ pass through $A$ and are perpendicular to (the extension of) $BC$. It is clear that there is no room in point $A$ for two such lines, so $AC' = AC$ and hence $C = C'$.
[Step 4: if $x = x'$ then $x$ has all the properties of $x'$, in particular property $Y$.] Since $C = C'$ and $C'$ lies on circle $c$ by definition, so does $C$, as we wanted to show.
Proof of theorem 3' (after René):
[Step 0, let an object x of type X with property Z be given. We want to show that it has property Y:] Let numbers $m, n$ be given such that $2^m - 1 | 2^n - 1$. We want to show that $m | n$. Since we are talking about dividing $n$ by $m$ we might as well do this division (with remainder) and write $n = qm + r$ for some integer $q$ and some integer $r < m$.  
[Step 1, construct an object $x'$ that is 'close' to $x$ but already has property $Y$:] We consider the number pair $(m, n')$ with $n' = qm$. It is close to $(m, n)$ in the sense that the smaller numbers in each pair are the same and the bigger numbers only differ by the tiny amount $r < m$. Also obviously $m|qm$.
[Step 2, by the non-reversed version of the theorem, object $x'$ also has property $Z$:] By Thm. 3 above, the number $2^m -1$ divides the the number $2^{qm}-1$. Multiplying the latter number with $2^r$ we find that $2^m - 1$ divides $2^n - 2^r$.
[Step 3, this town ain't big enough for two objects with property $Z$:] In particular, the town of numbers close to $2^n$ (recall that $2^r$ is small compared to $2^m$) is not big enough for more than one multiple of $2^m - 1$. Formally: since $2^m -1$ divides both $2^n -1$ and $2^n - 2^r$ it divides their difference $2^r - 1$. But since $2^r - 1 < 2^m - 1$ this can only happen when $2^r - 1 = 0$ which in turn only happens when $r = 0$ and hence $n' = n$.
[Step 4: if $x = x'$ then $x$ has all the properties of $x'$, in particular property $Y$.] If $r =0$ so that $n = qm$ then $m$ is a divisor of $n$ as desired.
Questions:


*

*Are there more examples of proofs that follow this scheme?  

*Is the use in an 'this town ain't big enough'-argument in some sense unavoidable when using an implication in the proof of its converse? In other words: are there proofs of equivalences $A \Leftrightarrow B$ where the proof of $\Leftarrow$ uses that $\Rightarrow$ holds (as in the examples above) but then in a rather different way, avoiding step 1 and 3?

*Given a bi-implication $A \Leftrightarrow B$ which we want to prove in this way, do we have a choice which direction to prove directly and which one based on the other direction? Or is there a clear preferred choice?
With respect to question 3: I believe that the latter holds for Thms 1 and 3 above but that for Thales and Reverse Thales we could have proceeded in the opposite way. The reason is that there every step in the 'direct' proof of Thm 2 is also reversible into a step in a direct proof of Thm 2', e.g. every isosceles triangle has two equal angles, but also every triangle with equal angles is isosceles. 
Motivation: I since long knew that in plane geometry there are more examples of this phenomenon than the two listed here. In particular I'm thinking of the generalizations of Thales/Reversed Thales replacing the right angle with an arbitrary but fixed angle $\alpha$ and the diameter by an arbitrary but fixed chord. (And the various strengthenings of those theorems.) However I was quite surprised to find an example (Thm. 3) from a completely different subfield of mathematics (number theory). So more examples from number theory or, even better, a yet different part of mathematics are most welcome.
(Finally two remarks on the naming of the theorems above: 


*

*Thm. 3 is generally not called 'Mersenne's theorem', but Mersenne is generally credited with finding that the only circumstances under which $2^n - 1$ can be a prime number is when $n$ is prime itself. That is essentially Thm. 3.

*Some sources use the names Thales' Theorem and Reverse Thales' Theorem in the way I do and some sources use the name Thales' Theorem for Theorem 2' and Reverse Thales' Theorem for theorem 2. The reason for this inconsistency lies, I believe, in what I write with regard to question 3 above. The use of Pythagoras' Theorem and Reverse Pythagoras Theorem on the other hand is unanimous throughout the literature as far as I know.


)
 A: Here are two answers that reached me trough other channels, one to question 1 (more examples of this phenomenon) and one to question 3 (is there a preferred choice as to which implication to prove directly and which using the other implication?).
As for question 1, my friend dr. Q sent me another beautiful result about triangles called Ceva's theorem. In a triangle, draw line segments from each angle to the opposite side, partitioning the three original sides of the triangle into six segments of lengths $a$ and $b$, $c$ and $d$, $e$ and $f$ respectively (so the original triangle had side lengths $a + b$, $c + d$ and $e + f$). Now Ceva's theorem asserts that whenever the three lines go through one point, the numbers $a, b, c, d, e, f$ satisfy $a/b * c/d * e/f = 1$. 
The proof is left to the reader, not because it is easy but because it is besides the point. The point is of course there is also a reverse Ceva theorem which can be proved by the scheme in the post. Reverse Ceva asserts that whenever the numbers $a, b, c, d, e, f$ satisfy $a/b * c/d * e/f = 1$ then the lines (used to define these numbers in the first place) go through one point.
Proof: choose two of the lines (say the ones defining $a, b$ and $c, d$) and construct a third line from the appropriate corner of the triangle through their intersection to the opposite side, dividing it into segments of length $e', f'$. Now by ordinary Ceva, $a/b * c/d * e'/f' = 1$, so $e'/f' = e/f$ so the new line was actually the third of the lines we already had and hence it already went through the intersection point of the other two.
Dr. Q also pointed out that the somewhat more famous theorems of Pascal and Menelaos (together with their converses) provide examples of this phenomenon as well.
As for question 3) there is a very interesting discussion going on at Math Educators SE where the OP asks for a proof or intuition for one special case of Reverse Pythagoras and most posters don't manage to avoid either using Ordinary Pythagoras or proving it as a free bonus in the process of answering. It seems in other words very clear that in case of Pythagoras/Reverse Pythagoras there is a very strongly preferred order in which to prove them. 
Then someone posts a link to an article in the Mathematical Gazette whose sole purpose is to answer the question whether Reverse Pythagoras can be proven without proving Ordinary Pythagoras first. The author finds a proof but it is much longer than any of the standard proofs of Pythagoras' Theorem and it uses, as the author points out, more advanced 'known' results from Euclid's elements than Euclid's proof of Pythagoras' theorem does. 
However, having given this elaborate proof of Reverse Pythagoras they deduce Ordinary Pythagoras from it quickly in almost exactly the way we did the opposite above, in particular by following the above scheme.
The lesson I took from this is this. Yes, in many cases there is a prefered choice as to which implication to prove directly and which by the above scheme, but no this has nothing to do with the scheme itself. It depends solely on for which of the two directions giving a direct proof is easier, the roles of Y and Z in the proof scheme are completely symmetric/interchangeable.
In retrospect this is obvious: if there is no room in this town for two X's with property Z and property Z is equivalent to property Y by the theorems we are trying to prove, then automatically there is no room for two X's with property Y either.
I consider question 3) as answered by this, but I'm still desperately looking for non-geometry examples for question 1) and any examples for question 2) so please respond.
