2010-09-19 - ひとり勉強会の練習問題。 ||<Require Import Arith Omega. Fixpoint sum (n: nat) := match n with | O => 0 | S m => n + sum m end. Theorem Sum_of_nat: forall (n m: nat), m = 2 * sum n -> m = n*(n+1). Proof. intro n. induction n. (以下は練習問題) なんとか解けたけどかなり苦戦した。三日かかった。 Require </require>…