Let m be given.
Assume Hm.
Let n be given.
Assume Hn.
Apply ordinal_In_Or_Subq n 1 (nat_p_ordinal n Hn) (nat_p_ordinal 1 nat_1) to the current goal.
Assume H1: n ∈ 1.
Apply orIL to the current goal.
We will prove n = 0.
Apply cases_1 n H1 to the current goal.
We will prove 0 = 0.
Use reflexivity.
Assume H1: 1 ⊆ n.
Apply orIR to the current goal.
We will prove m ⊆ m * n.
rewrite the current goal using mul_nat_1R m (from right to left) at position 1.
We will prove m * 1 ⊆ m * n.
An exact proof term for the current goal is mul_nat_Subq_L 1 n nat_1 Hn H1 m Hm.
∎