Apply nat_inv_impred to the current goal.
Let n be given.
Assume _.
Assume H1: 0 ∈ 0.
We will prove False.
An exact proof term for the current goal is EmptyE 0 H1.
Let m be given.
Assume Hm: nat_p m.
We will prove ∀n, nat_p n → 0 ∈ ordsucc m → 1 ∈ n → ordsucc m ∈ ordsucc m * n.
Apply nat_inv_impred to the current goal.
Assume _.
Assume H1: 1 ∈ 0.
We will prove False.
An exact proof term for the current goal is In_no2cycle 0 1 In_0_1 H1.
We will prove ∀n, nat_p n → 0 ∈ ordsucc m → 1 ∈ ordsucc n → ordsucc m ∈ ordsucc m * ordsucc n.
Apply nat_inv_impred to the current goal.
Assume _.
Assume H1: 1 ∈ 1.
We will prove False.
An exact proof term for the current goal is In_irref 1 H1.
Let n be given.
Assume Hn: nat_p n.
Assume _ _.
We will prove ordsucc m ∈ ordsucc m * ordsucc (ordsucc n).
rewrite the current goal using mul_nat_SR (ordsucc m) (ordsucc n) (nat_ordsucc n Hn) (from left to right).
We will prove ordsucc m ∈ ordsucc m + ordsucc m * ordsucc n.
rewrite the current goal using add_nat_0R (ordsucc m) (from right to left) at position 1.
We will prove ordsucc m + 0 ∈ ordsucc m + ordsucc m * ordsucc n.
Apply add_nat_In_L (ordsucc m) (nat_ordsucc m Hm) (ordsucc m * ordsucc n) (mul_nat_p (ordsucc m) (nat_ordsucc m Hm) (ordsucc n) (nat_ordsucc n Hn)) 0 to the current goal.
We will prove 0 ∈ ordsucc m * ordsucc n.
rewrite the current goal using mul_nat_SL m Hm (ordsucc n) (nat_ordsucc n Hn) (from left to right).
We will prove 0 ∈ m * ordsucc n + ordsucc n.
rewrite the current goal using add_nat_SR (m * ordsucc n) n Hn (from left to right).
We will prove 0 ∈ ordsucc (m * ordsucc n + n).
Apply nat_0_in_ordsucc to the current goal.
We will prove nat_p (m * ordsucc n + n).
An exact proof term for the current goal is add_nat_p (m * ordsucc n) (mul_nat_p m Hm (ordsucc n) (nat_ordsucc n Hn)) n Hn.
∎