Let x and y be given.
Assume HxS: SNo x.
Assume HyS: SNo y.
Assume H0lex: 0 ≤ x.
Assume Hypos: 0 < y.
We will prove 0 ≤ div_SNo x y.
We prove the intermediate claim HdivS: SNo (div_SNo x y).
An exact proof term for the current goal is (SNo_div_SNo x y HxS HyS).
Apply (SNoLt_trichotomy_or_impred (div_SNo x y) 0 HdivS SNo_0 (0 ≤ div_SNo x y)) to the current goal.
Assume Hdivlt0: div_SNo x y < 0.
We prove the intermediate claim Hxlt0y: x < mul_SNo 0 y.
An exact proof term for the current goal is (div_SNo_pos_LtL' x y 0 HxS HyS SNo_0 Hypos Hdivlt0).
We prove the intermediate claim Hxlt0: x < 0.
rewrite the current goal using (mul_SNo_zeroL y HyS) (from right to left) at position 1.
An exact proof term for the current goal is Hxlt0y.
We prove the intermediate claim Hxle0: x ≤ 0.
An exact proof term for the current goal is (SNoLtLe x 0 Hxlt0).
We prove the intermediate claim Heq0: x = 0.
An exact proof term for the current goal is (SNoLe_antisym x 0 HxS SNo_0 Hxle0 H0lex).
We prove the intermediate claim H00: 0 < 0.
rewrite the current goal using Heq0 (from right to left) at position 1.
An exact proof term for the current goal is Hxlt0.
An exact proof term for the current goal is (FalseE ((SNoLt_irref 0) H00) (0 ≤ div_SNo x y)).
Assume Hdiv0: div_SNo x y = 0.
rewrite the current goal using Hdiv0 (from left to right).
An exact proof term for the current goal is (SNoLe_ref 0).
Assume H0ltdiv: 0 < div_SNo x y.
An exact proof term for the current goal is (SNoLtLe 0 (div_SNo x y) H0ltdiv).
∎