Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
Assume H1: m * n = 2.
We prove the intermediate claim L1: m ⊆ 2.
Apply mul_nat_0_or_Subq m Hm n Hn to the current goal.
Assume H2: n = 0.
We will prove False.
Apply neq_2_0 to the current goal.
We will prove 2 = 0.
rewrite the current goal using H1 (from right to left).
We will prove m * n = 0.
rewrite the current goal using H2 (from left to right).
We will prove m * 0 = 0.
Apply mul_nat_0R to the current goal.
Assume H2: m ⊆ m * n.
We will prove m ⊆ 2.
rewrite the current goal using H1 (from right to left).
An exact proof term for the current goal is H2.
Apply nat_le2_cases m Hm L1 to the current goal.
Assume H.
Apply H to the current goal.
Assume H2: m = 0.
We will prove False.
Apply neq_2_0 to the current goal.
We will prove 2 = 0.
rewrite the current goal using H1 (from right to left).
We will prove m * n = 0.
rewrite the current goal using H2 (from left to right).
We will prove 0 * n = 0.
An exact proof term for the current goal is mul_nat_0L n Hn.
Assume H2: m = 1.
Apply orIL to the current goal.
An exact proof term for the current goal is H2.
Assume H2: m = 2.
Apply orIR to the current goal.
An exact proof term for the current goal is H2.
∎