Apply nat_inv_impred to the current goal.

We will prove ∀n, nat_p n → 0 * n = 0 → 0 = 0 ∨ n = 0.

Let n be given.

Assume Hn _.

Apply orIL to the current goal.

Use reflexivity.

Let m be given.

Assume Hm: nat_p m.

Apply nat_inv_impred to the current goal.

Assume _.

Apply orIR to the current goal.

Use reflexivity.

Let n be given.

Assume Hn: nat_p n.

We will prove ordsucc m * ordsucc n = 0 → ordsucc m = 0 ∨ ordsucc n = 0.

rewrite the current goal using mul_nat_SR (ordsucc m) n Hn (from left to right).

We will prove ordsucc m + ordsucc m * n = 0 → ordsucc m = 0 ∨ ordsucc n = 0.

rewrite the current goal using add_nat_SL m Hm (ordsucc m * n) (mul_nat_p (ordsucc m) (nat_ordsucc m Hm) n Hn) (from left to right).

We will prove ordsucc (m + ordsucc m * n) = 0 → ordsucc m = 0 ∨ ordsucc n = 0.

Assume H1: ordsucc (m + ordsucc m * n) = 0.

We will prove False.

An exact proof term for the current goal is neq_ordsucc_0 (m + ordsucc m * n) H1.

∎