Make a command start new line in a list if it is not currently at the end of another list

I am trying to typeset a structured proof as demonstrated by Leslie Lamport in his paper How to Write a 21st Century Proof. In particular, I am trying to typeset Figure 3 (shown below).

My code and the output is shown below.

\documentclass[12pt,letterpaper]{article}

\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{enumitem}

% LSP is short for Lamport Structured Proof
\newlist{lsp}{enumerate}{10}
\setlist[lsp]{label=\arabic*.}
\newcommand{\lspproof}{{\scshape Proof:\ \ }}
\newcommand{\lspqed}{Q.E.D.}

\newtheorem{corollary}{Corollary}

\begin{document}

\begin{corollary}
If $f'(x) > 0$ for all $x$ on an interval $I$,
then $f$ is increasing on $I$.
\end{corollary}

\begin{lsp}
\item It suffices to assume
\begin{lsp}
\item $a$ and $b$ are points in $I$
\item $a < b$
\end{lsp}
\lspproof By definition of an increasing function

\item There is some $x$ in $(a,b)$
with $\displaystyle f'(x) = \frac{f(b)-f(a)}{b-a}$.\\*
\lspproof By assumptions 1.1 and 1.2,
the hypothesis that $f$ is differentiable on $I$,
and the Mean Value Theorem.

\item $f'(x) > 0$ for all $x$ in $(a,b)$.\\*
\lspproof By the induction hypothesis of the corollary and assumption 1.1.

\item $\displaystyle \frac{f(b)-f(a)}{b-a} > 0$\\*
\lspproof By 2 and 3.

\item \lspqed\\*
\lspproof Assumption 1.2 implies $b - a > 0$,
so 4 implies $f(b) - f(a) > 0$,
which implies $f(b) > f(a)$.
By 1, this proves the corollary
\end{lsp}

\end{document}


While I am quite happy with the result, I find it a bit irritating that I have to manually tell LaTeX to start a new line using \\* before each \lspproof.

Questions:

1. Is there a way to define \lspproof such that it will automatically start a new line when needed? Notice that I did not need to insert \\* before the "Proof:" in step 1 because the "Proof:" occurs after an enumerate environment.
2. Is there a way to slightly increase the vertical space between the "Proof." from \lspproof and the previous line?
• We could just ask Leslie for the code :-) – Joseph Wright Feb 28 '14 at 22:23
• I don't know him personally, or rather I know who he is but he doesn't know who I am. However, I would love it for you or anyone else to ask him. :-) – I Like to Code Feb 28 '14 at 22:25

Here's one option that uses a paragraph break rather than a forced line break:

\documentclass[12pt,letterpaper]{article}

\usepackage{amsmath,amsthm,enumitem}

% LSP is short for Lamport Structured Proof
\newlist{lsp}{enumerate}{10}
\setlist[lsp]{label=\arabic*.,ref=\arabic*}
\newcommand{\lspqed}{Q.E.D.}

\newtheorem{corollary}{Corollary}

\begin{document}

\begin{corollary}
If $f'(x) > 0$ for all $x$ on an interval~$I$, then $f$ is increasing on~$I$.
\end{corollary}

\begin{lsp}
\item It suffices to assume \label{proof1}
\begin{lsp}
\item $a$ and~$b$ are points in~$I$ \label{assump1}
\item $a < b$ \label{assump2}
\end{lsp}
\lspproof By definition of an increasing function.

\item There is some~$x$ in $(a,b)$ with $f'(x) = \dfrac{f(b)-f(a)}{b-a}$. \label{proof2}
\lspproof By assumptions~\ref{proof1}.\ref{assump1} and~\ref{proof1}.\ref{assump2}, the hypothesis that~$f$ is differentiable on~$I$,
and the Mean Value Theorem.

\item $f'(x) > 0$ for all $x$ in $(a,b)$. \label{proof3}
\lspproof By the induction hypothesis of the corollary and assumption~\ref{proof1}.\ref{assump1}.

\item $\dfrac{f(b)-f(a)}{b-a} > 0$ \label{proof4}
\lspproof By~\ref{proof2} and~\ref{proof3}.

\item \lspqed
\lspproof Assumption~\ref{proof1}.\ref{assump2} implies $b - a > 0$, so~\ref{proof4} implies $f(b) - f(a) > 0$, which implies $f(b) > f(a)$.
By~\ref{proof1}, this proves the corollary
\end{lsp}

\end{document}