Let a and b be given.
Assume H1: ordsucc a = ordsucc b.
We prove the intermediate claim L1: a ∈ ordsucc b.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is (ordsuccI2 a).
Apply (ordsuccE b a L1) to the current goal.
Assume H2: a ∈ b.
We prove the intermediate claim L2: b ∈ ordsucc a.
rewrite the current goal using H1 (from left to right).
An exact proof term for the current goal is (ordsuccI2 b).
Apply (ordsuccE a b L2) to the current goal.
Assume H3: b ∈ a.
We will prove False.
An exact proof term for the current goal is (In_no2cycle a b H2 H3).
Assume H3: b = a.
Use symmetry.
An exact proof term for the current goal is H3.
Assume H2: a = b.
An exact proof term for the current goal is H2.
∎