Assume _.

Assume H1: Pi_nat f 0 = 0.

We will prove False.

Apply neq_1_0 to the current goal.

We will prove 1 = 0.

Use transitivity with and Pi_nat f 0.

We will prove 1 = Pi_nat f 0.

Use symmetry.

An exact proof term for the current goal is Pi_nat_0 f.

We will prove Pi_nat f 0 = 0.

An exact proof term for the current goal is H1.

Let n be given.

Assume Hn: nat_p n.

Assume IHn: (∀i ∈ n, nat_p (f i)) → Pi_nat f n = 0 → ∃i ∈ n, f i = 0.

Assume Hf: ∀i ∈ ordsucc n, nat_p (f i).

rewrite the current goal using Pi_nat_S f n Hn (from left to right).

Assume H1: Pi_nat f n * f n = 0.

We will prove ∃i ∈ ordsucc n, f i = 0.

We prove the intermediate claim L1: ∀i ∈ n, nat_p (f i).

Let i be given.

Assume Hi.

Apply Hf to the current goal.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

We prove the intermediate claim L2: nat_p (f n).

Apply Hf to the current goal.

Apply ordsuccI2 to the current goal.

We prove the intermediate claim L3: nat_p (Pi_nat f n).

An exact proof term for the current goal is Pi_nat_p f n Hn L1.

Apply mul_nat_0_inv (Pi_nat f n) L3 (f n) L2 H1 to the current goal.

Assume H2: Pi_nat f n = 0.

Apply IHn L1 H2 to the current goal.

Let i be given.

Assume H.

Apply H to the current goal.

Assume Hi: i ∈ n.

Assume H3: f i = 0.

We use i to witness the existential quantifier.

Apply andI to the current goal.

We will prove i ∈ ordsucc n.

Apply ordsuccI1 to the current goal.

An exact proof term for the current goal is Hi.

We will prove f i = 0.

An exact proof term for the current goal is H3.

Assume H2: f n = 0.

We use n to witness the existential quantifier.

Apply andI to the current goal.

We will prove n ∈ ordsucc n.

Apply ordsuccI2 to the current goal.

We will prove f n = 0.

An exact proof term for the current goal is H2.