Let alpha, beta, p and q be given.
Assume Ha Hb.
Assume H1: PNoLt alpha p 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.
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.
An exact proof term for the current goal is Hb.