���Ƥμ����ѻ���ܤ��̤��ޤ���������Dz�����������Ŭ�ڤȹͤ�������� �����Ǥ������Ƥ��ޤ��󡥤��Τ��������ޤ����ޤ��ֵ�������������ȹͤ��� �������ˤĤ��Ƥ�������Ƥ��ޤ��󡥲�����Ǽ���Ǥ��ʤ����ϡ��ޤ����� �����������ޤ�����������ϤҤȤĤˤޤȤ᤿�ꡤ�����ʸ�Ϥ�Ŭ���ѹ����� ���ޤ���
m : nat ... IHn' : ... m �˸��ڤ�����Ǽˡ�β��� ... (Q(m) �ȸƤ�) ... ====================================== ������̿�� G(m)���ơ��ֵ��Ǥ����������褦�ˡ�����Ū��Ǽˡ�������Ǥ�դ� m �ˤĤ��� P(m)�פ�������뤿�����ˡ�Ǥ������Ρ�Ǥ�դ� m �ˤĤ��ơפ���ʬ��ʸ̮�� ���� m : nat ���������Ƥ��ޤ�������������ξ����ϡ��¤ϡ���Ǥ�դ� m �� �Ĥ��� G(m)�פǤϤʤ�����Ǥ�դ� m �ˤĤ��ơ�Q(m) �ʤ�� G(m)�פȤ����� �������夤̿���������褦�Ȥ��뤳�Ȥ��������Ƥ��ޤ����Ǥ��Τǡ������� induction m �򤷤Ƥ⡤Coq �ϡ�Q(m) �ʤ�� G(m)�פ��P(m)�פȹͤ��ƿ��� ���������������Ƥ��ޤ������η�̤��ޤ������Ǥ��ʤ����Ȥ������Ȥˤʤ� �����Ǥ��� �������򤹤뤿��ˤ� IHn' ��ʸ̮����ä��Ƥ��� induction m �򤹤롤 �Ȥ�����⤢��ΤǤ����������Ƥ��ξ��ϡ���ö����������������äơ� ��Ǥ�դ� m �ˤĤ��� G(m)�פȤ��������������Ω�Ƥ��������ޤ������Ȼפ��ޤ���
Error: No focused proof (No proof-editing in progress).�Τ褦�˥��顼�ˤʤ뤳��(������ǤϤʤ�����)���ǧ���Ƥ��������� ����¾�θ����Ȥ��ơ�
Inductive sum (n : nat) : nat := match n with | O => O | S p => n + sum p.