部分関数禁止の理由にカリー・ハワード同型対応の観点からの補足を追加

[Copilot]

既存の説明（非停止関数を許すと False が証明できる）に加えて、より根本的な理由としてカリー・ハワード同型対応の観点——「帰納法は再帰に対応する」——からの補足説明を追記する。

変更点

• LeanByExample/Modifier/DecreasingBy.lean の「部分関数を禁止するのはなぜか？」セクションに、カリー・ハワード同型対応による説明段落を追加
• 無限再帰による直接的な偽命題の証明を示す proofLoop の例を追加

-- unsafe を使うと、証明の中で無限再帰（= 終わらない帰納法）が使える
unsafe def proofLoop (P : Prop) : P := proofLoop P

-- その結果、False のような矛盾した命題でも「証明」できてしまう
unsafe example : False := proofLoop False

既存の search/anything 経由の例と異なり、proofLoop は「証明 ＝ 再帰関数」を直接示すため、帰納法との対応がより明確になる。