Let x be given.
Assume Hx Hxpos.
Let g be given.
Assume Hg.
Apply and3I to the current goal.
Let y be given.
Assume Hy.
Let k be given.
Assume Hk.
Assume H2 _.
Apply H2 y H1 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let y be given.
Assume Hy.
Let k be given.
Assume Hk.
Assume _ H2.
Apply H2 y H1 to the current goal.
Assume H3 _.
An exact proof term for the current goal is H3.
Let w be given.
Assume Hw.
Let z be given.
Assume Hz.
Let k be given.
Assume Hk.
Assume H2 _.
Apply H2 w H1 to the current goal.
Let k' be given.
Assume Hk'.
Assume _ H6.
Apply H6 z H5 to the current goal.
An exact proof term for the current goal is H9.
We will
prove x * z ≤ x * w.
An exact proof term for the current goal is H4.
∎