数直線（高校数学）

方針：実数から点が 1 つ決まることと、点から実数が 1 つ決まることを、別々に確かめる。
段 1（実数から点へ）。$a>0$ なら、rem-nlh-axioms の性質 1 により、正の側に $OP=a$ の点 $P$ はちょうど 1 つある。$a< 0$ なら $-a>0$ なので、負の側に $OP=-a$ の点がちょうど 1 つある。$a=0$ なら点は $O$ だけである。どの場合も、座標が $a$ の点はちょうど 1 つある。
段 2（点から実数へ）。直線の上の点 $P$ をとる。$P=O$ なら座標は $0$ である。$P\ne O$ なら、$P$ は正の側か負の側のどちらか一方にある。正の側なら $a:=OP>0$ とおくと、$P$ は定義の 1 の点なので座標は $a$ である。負の側なら $a:=-OP< 0$ とおくと、定義の 2 の点なので座標は $a$ である。
段 3（座標がただ 1 つであること）。$P$ の座標が $a$ とも $b$ とも言えたとすると、$\overline{OP}=a$ かつ $\overline{OP}=b$ なので $a=b$ である。$\square$

方針：rem-nlh-axioms の性質 2 を、$A$、$O$、$B$ の 3 点に使う。
段 1（1 の証明）。性質 2 を $A$、$O$、$B$ に使うと $\overline{AB}=\overline{AO}+\overline{OB}$ である。$\overline{AO}=-\overline{OA}=-a$、$\overline{OB}=b$（座標は原点からの向きつきの長さ）なので、$\overline{AB}=-a+b=b-a$ である。
段 2（2 の証明）。向きつきの長さの定義から、$\overline{AB}$ は $AB$ か $-AB$ か $0$（$A=B$ のとき）のどれかで、どの場合も $|\overline{AB}|=AB$ である。段 1 から $AB=|b-a|$ となる。
段 3（3 の証明）。$A\ne B$ とする。$B$ が $A$ から見て正の向きにあることは、定義により $\overline{AB}=AB>0$ ということである。負の向きにあれば $\overline{AB}=-AB< 0$ である。段 1 から $\overline{AB}=b-a$ なので、正の向きにあることは $b-a>0$、つまり $a< b$ と同値である。$\square$

方針：$M$ の座標を $m$ とおき、thm-nlh-distance で $AM=MB$ を $m$ の式にする。
段 1。thm-nlh-distance の 2 により、$AM=|m-a|$、$MB=|b-m|$ である。2 つの実数の絶対値が等しいのは、2 つが等しいか、符号だけ違うときなので、$AM=MB$ は
$$ m-a=b-m\quad\text{または}\quad m-a=-(b-m) $$
と同値である。
段 2。後の式を整理すると $m-a=m-b$、つまり $a=b$ となり、$A\ne B$ に反する。したがって後の式は起こらない。
段 3。前の式を整理すると $2m=a+b$、$m=\dfrac{a+b}2$ である。逆に $m=\dfrac{a+b}2$ なら $m-a=\dfrac{b-a}2=b-m$ なので、$AM=MB$ が成り立つ。thm-nlh-bijection により座標が $\dfrac{a+b}2$ の点はちょうど 1 つなので、中点はちょうど 1 つである。$\square$

方針：thm-nlh-distance で距離を $|x-c|$ と書き、$|u|< r$ と $-r< u< r$ が同値であることを示す。
段 1。点 $x$ と点 $c$ の距離は thm-nlh-distance により $|x-c|$ である。$u:=x-c$ とおく。
段 2（$|u|< r$ なら $-r< u< r$）。$u\ge0$ なら $u=|u|< r$ で、$-r< 0\le u$ である。$u< 0$ なら $-u=|u|< r$ の両辺に $-1$ を掛けて $u>-r$ で、$u< 0< r$ である。どちらでも $-r< u< r$ となる。
段 3（$-r< u< r$ なら $|u|< r$）。$u\ge0$ なら $|u|=u< r$。$u< 0$ なら $|u|=-u$ で、$-r< u$ の両辺に $-1$ を掛けて $-u< r$ である。
段 4。$-r< x-c< r$ の各辺に $c$ を足すと $c-r< x< c+r$ である。$\square$

方針：新しい座標は、新しい原点からの向きつきの長さを、新しい単位の長さで割り、新しい正の向きで符号を付けたものである。
段 1（新しい単位と向き）。thm-nlh-distance により、$O'E'=|(c+u)-c|=|u|$ である。新しい正の向きは $O'$ から $E'$ への向きで、これは $u>0$ なら元の正の向き、$u< 0$ なら元の負の向きである。
段 2（$u>0$ のとき）。向きが同じなので、新しい単位で測った向きつきの長さは、元の向きつきの長さを $u$ で割ったものである。thm-nlh-distance の 1 により $\overline{O'P}=x-c$ なので、$x'=\dfrac{x-c}{u}$ である。
段 3（$u< 0$ のとき）。向きが逆なので、元の向きつきの長さ $x-c$ の符号を変え、新しい単位 $|u|=-u$ で割る。$x'=\dfrac{-(x-c)}{-u}=\dfrac{x-c}{u}$ で、段 2 と同じ式になる。
段 4。$x'=\dfrac{x-c}u$ の両辺に $u$ を掛けて $c$ を足すと $x=c+ux'$ である。$\square$

方針：まず $f(0)=0$ の場合に、$f(1)$ の符号が全体を決めることを示し、最後に一般の場合をこれに帰着させる。
段 1（$f(0)=0$ の場合の準備）。$f(0)=0$ とする。$y=0$ とおくと $|f(x)|=|x|$ なので、各 $x$ について $f(x)=x$ か $f(x)=-x$ である。特に $s:=f(1)$ は $1$ か $-1$ である。
段 2（$f(x)=sx$ を示す）。$x$ を 1 つとり、$f(x)=-sx$ だったとする。$y=1$ とおいた式 $|f(x)-f(1)|=|x-1|$ に代入すると、$|-sx-s|=|x-1|$ である。左辺は $|s|\cdot|x+1|=|x+1|$ なので $|x+1|=|x-1|$、両辺を 2 乗して $x^2+2x+1=x^2-2x+1$、$x=0$ である。$x=0$ なら $-sx=sx=0$ である。したがって、どの $x$ でも $f(x)=sx$ である。
段 3（一般の場合）。$c:=f(0)$ とし、$g(x):=f(x)-c$ とおく。$g(x)-g(y)=f(x)-f(y)$ なので $g$ も条件を満たし、$g(0)=0$ である。段 1・2 により $g(x)=sx$（$s=\pm1$）で、$f(x)=c+sx$ となる。$\square$