In a text there will often be a few important results that are usually called Theorems. Intermediate statements are called Lemmas, and statements that follow immediately from previous results are called Corollaries.

There is a problem here, however. Especially in the context of theorem provers: A Theorem $A$ is often proved using induction. In order to perform this induction, the statement of the theorem needs to be strengthened to $B$ (otherwise the induction will not 'go through'). The original statement $A$ of the theorem will then follow trivially from $B$. We now have three possible naming conventions for this:

• Call $B$ a Lemma and $A$ a Theorem. This is attractive, because $B$ is the main statement of interest. The problem is, however, that the proof of $A$ is mainly done in $B$, which is now called an 'unimportant' Lemma.

• Call $B$ a Theorem and $A$ a Corollary. This is attractive because $B$ follows immediately from $A$, hence a Corollary. Also, it makes clear that the proof of $B$ contains a lot of important steps. However, when looking over the text quickly, one might miss the main statement $A$, because it is phrased as a simple consequence of $B$.

• A third option is to not have $B$ at all but only state Theorem $A$, and then perform the strengthening of the statement 'inline' in the proof via a cut. This is also inconvenient because it hides the technique used to prove $B$, which may be very important.

I would be interested in how this is commonly solved.

In a text there will often be a few important results that are usually called Theorems. Intermediate statements are called Lemmas, and statements that follow immediately from previous results are called Corollaries.

There is a problem here, however. Especially in the context of theorem provers: A Theorem $A$ is often proved using induction. In order to perform this induction, the statement of the theorem needs to be strengthened to $B$ (otherwise the induction will not 'go through'). The original statement $A$ of the theorem will then follow trivially from $B$. We now have three possible naming conventions for this:

• Call $B$ a Lemma and $A$ a Theorem. This is attractive, because $A$ is the main statement of interest. The problem is, however, that the proof of $A$ is mainly done in $B$, which is now called an 'unimportant' Lemma.

• Call $B$ a Theorem and $A$ a Corollary. This is attractive because $A$ follows immediately from $B$, hence a Corollary. Also, it makes clear that the proof of $B$ contains a lot of important steps. However, when looking over the text quickly, one might miss the main statement $A$, because it is phrased as a simple consequence of $B$.

• A third option is to not have $B$ at all but only state Theorem $A$, and then perform the strengthening of the statement 'inline' in the proof via a cut. This is also inconvenient because it hides the technique used to prove $B$, which may be very important.

I would be interested in how this is commonly solved.

In a text there will often be a few important results that are usually called Theorems. Intermediate statements are called Lemmas, and statements that follow immediately from previous results are called Corollaries.

There is a problem here, however. Especially in the context of theorem provers: A Theorem $A$ is often proved using induction. In order to perform this induction, the statement of the theorem needs to be strengthened to $B$ (otherwise the induction will not 'go through'). The original statement $A$ of the theorem will then follow trivially from $B$. We now have three possible naming conventions for this:

• Call $B$ a Lemma and $A$ a Theorem. This is attractive, because $B$ is the main statement of interest. The problem is, however, that the proof of $B$ is mainly done in $A$, which is now called an 'unimportant' Lemma.

• Call $B$ a Theorem and $A$ a Corollary. This is attractive because $B$ follows immediately from $A$, hence a Corollary. Also, it makes clear that the proof of $A$ contains a lot of important steps. However, when looking over the text quickly, one might miss the main statement $B$, because it is phrased as a simple consequence of $A$.

• A third option is to not have $B$ at all but only state Theorem $A$, and then perform the strengthening of the statement 'inline' in the proof via a cut. This is also inconvenient because it hides the technique used to prove $B$, which may be very important.

I would be interested in how this is commonly solved.

In a text there will often be a few important results that are usually called Theorems. Intermediate statements are called Lemmas, and statements that follow immediately from previous results are called Corollaries.

There is a problem here, however. Especially in the context of theorem provers: A Theorem $A$ is often proved using induction. In order to perform this induction, the statement of the theorem needs to be strengthened to $B$ (otherwise the induction will not 'go through'). The original statement $A$ of the theorem will then follow trivially from $B$. We now have three possible naming conventions for this:

• Call $B$ a Lemma and $A$ a Theorem. This is attractive, because $B$ is the main statement of interest. The problem is, however, that the proof of $A$ is mainly done in $B$, which is now called an 'unimportant' Lemma.

• Call $B$ a Theorem and $A$ a Corollary. This is attractive because $B$ follows immediately from $A$, hence a Corollary. Also, it makes clear that the proof of $B$ contains a lot of important steps. However, when looking over the text quickly, one might miss the main statement $A$, because it is phrased as a simple consequence of $B$.

• A third option is to not have $B$ at all but only state Theorem $A$, and then perform the strengthening of the statement 'inline' in the proof via a cut. This is also inconvenient because it hides the technique used to prove $B$, which may be very important.

I would be interested in how this is commonly solved.