Let m and n be given.
Assume H1m: 1 ∈ m.
Assume H1: divides_nat m n.
Assume H2: divides_nat m (ordsucc n).
Apply H1 to the current goal.
Assume H.
Apply H to the current goal.
Assume Hm: m ∈ ω.
Assume Hn: n ∈ ω.
Assume H.
Apply H to the current goal.
Let k be given.
Assume H.
Apply H to the current goal.
Assume Hk: k ∈ ω.
Assume Hmk: m * k = n.
Apply H2 to the current goal.
Assume _ H.
Apply H to the current goal.
Let k' be given.
Assume H.
Apply H to the current goal.
Assume Hk': k' ∈ ω.
Assume Hmk': m * k' = ordsucc n.
We prove the intermediate claim Lm: nat_p m.
An exact proof term for the current goal is omega_nat_p m Hm.
We prove the intermediate claim Ln: nat_p n.
An exact proof term for the current goal is omega_nat_p n Hn.
We prove the intermediate claim Lk: nat_p k.
An exact proof term for the current goal is omega_nat_p k Hk.
We prove the intermediate claim Lk': nat_p k'.
An exact proof term for the current goal is omega_nat_p k' Hk'.
We prove the intermediate claim L1: 1 + n = ordsucc n.
rewrite the current goal using add_nat_SL 0 nat_0 n Ln (from left to right).
We will prove ordsucc (0 + n) = ordsucc n.
Use f_equal.
An exact proof term for the current goal is add_nat_0L n Ln.
We prove the intermediate claim L2: m * k' ∈ m + n.
rewrite the current goal using Hmk' (from left to right).
We will prove ordsucc n ∈ m + n.
rewrite the current goal using L1 (from right to left).
We will prove 1 + n ∈ m + n.
An exact proof term for the current goal is add_nat_In_R m Lm 1 H1m n Ln.
We prove the intermediate claim L3: m + n ⊆ m * k'.
rewrite the current goal using Hmk (from right to left).
We will prove m + m * k ⊆ m * k'.
rewrite the current goal using mul_nat_SR m k Lk (from right to left).
We will prove m * ordsucc k ⊆ m * k'.
Apply mul_nat_Subq_L to the current goal.
Apply nat_ordsucc to the current goal.
An exact proof term for the current goal is Lk.
An exact proof term for the current goal is Lk'.
We will prove ordsucc k ⊆ k'.
Apply ordinal_In_Or_Subq k k' (nat_p_ordinal k Lk) (nat_p_ordinal k' Lk') to the current goal.
Assume H3: k ∈ k'.
An exact proof term for the current goal is ordinal_ordsucc_In_Subq k' (nat_p_ordinal k' Lk') k H3.
Assume H3: k' ⊆ k.
We will prove False.
We prove the intermediate claim L3a: ordsucc n ⊆ n.
rewrite the current goal using Hmk' (from right to left).
rewrite the current goal using Hmk (from right to left).
We will prove m * k' ⊆ m * k.
An exact proof term for the current goal is mul_nat_Subq_L k' k Lk' Lk H3 m Lm.
Apply In_irref n to the current goal.
We will prove n ∈ n.
Apply L3a to the current goal.
We will prove n ∈ ordsucc n.
Apply ordsuccI2 to the current goal.
An exact proof term for the current goal is Lm.
Apply In_irref (m * k') to the current goal.
Apply L3 to the current goal.
An exact proof term for the current goal is L2.
∎