>>148
妥当な証明を書きまくるというか、公理やすでに証明された論理式に推論規則を
適用しまくって目的のものにたどり着くまで待つって感じか。

∀x∃y(sx=y∧x<y)|-sa=b∧a<b

∀x∃y(sx=y∧x<y)|-sb=c∧b<c

sa=b∧a<b∧sb=c∧b<c|-∀x∃y∃z(sx=y∧x<y∧sy=z∧y<z)

例化や量化の手順は端折ってるがこんな具合。
後者関数の公理だけから出発して例化と量化を適用してるだけだし、
なんとかなるんじゃ、後者の後者のほうが大きいことを証明するだけなら。