証明戦略unfoldとfoldの練習です。 Coq < Lemma pluszero: forall n:nat, plus n 0 = n. 1 subgoal ============================ forall n : nat, n + 0 = n pluszero < intros. 1 subgoal n : nat ============================ n + 0 = n pluszero < indu…