We will prove m * 0 ⊆ n * 0.

rewrite the current goal using mul_nat_0R (from left to right).

Apply Subq_ref to the current goal.

Let k be given.

Assume Hk: nat_p k.

Assume IHk: m * k ⊆ n * k.

We will prove m * ordsucc k ⊆ n * ordsucc k.

rewrite the current goal using mul_nat_SR m k Hk (from left to right).

rewrite the current goal using mul_nat_SR n k Hk (from left to right).

We will prove m + m * k ⊆ n + n * k.

Apply Subq_tra (m + m * k) (m + n * k) (n + n * k) to the current goal.

We will prove m + m * k ⊆ m + n * k.

Apply add_nat_Subq_L m Hm (m * k) (mul_nat_p m Hm k Hk) (n * k) (mul_nat_p n Hn k Hk) to the current goal.

We will prove m * k ⊆ n * k.

An exact proof term for the current goal is IHk.

We will prove m + n * k ⊆ n + n * k.

An exact proof term for the current goal is add_nat_Subq_R m Hm n Hn Hmn (n * k) (mul_nat_p n Hn k Hk).