2008-10-28 Seven Trees を… Coq Require Import ZArith. Open Scope Z_scope. Goal forall t:Z, t = 1 + t^2 -> t^7 = t. intros. ring [H].終わらない…