Let alpha, beta, p and q be given.
Assume Ha Hb.
Assume H1: PNoLt alpha p beta q.
We will prove PNoLt (SNoLev (PSNo alpha p)) (λgamma ⇒ gamma ∈ PSNo alpha p) (SNoLev (PSNo beta q)) (λgamma ⇒ gamma ∈ PSNo beta q).
rewrite the current goal using SNoLev_PSNo alpha Ha p (from left to right).
rewrite the current goal using SNoLev_PSNo beta Hb q (from left to right).
We will prove PNoLt alpha (λgamma ⇒ gamma ∈ PSNo alpha p) beta (λgamma ⇒ gamma ∈ PSNo beta q).
Apply PNoEqLt_tra alpha beta Ha Hb (λgamma ⇒ gamma ∈ PSNo alpha p) p (λgamma ⇒ gamma ∈ PSNo beta q) to the current goal.
We will prove PNoEq_ alpha (λgamma ⇒ gamma ∈ PSNo alpha p) p.
Apply PNoEq_PSNo to the current goal.
An exact proof term for the current goal is Ha.
We will prove PNoLt alpha p beta (λgamma ⇒ gamma ∈ PSNo beta q).
Apply PNoLtEq_tra alpha beta Ha Hb p q (λgamma ⇒ gamma ∈ PSNo beta q) to the current goal.
An exact proof term for the current goal is H1.
We will prove PNoEq_ beta q (λgamma ⇒ gamma ∈ PSNo beta q).
Apply PNoEq_sym_ to the current goal.
Apply PNoEq_PSNo to the current goal.
An exact proof term for the current goal is Hb.
∎