Let L, alpha, beta, p and q be given.

Assume Ha Hb.

Assume H1: PNo_downc L alpha p.

Assume H2: PNoLe beta q alpha p.

We will prove PNo_downc L beta q.

Apply H1 to the current goal.

Let gamma be given.

Assume H3.

Apply H3 to the current goal.

Assume Hc: ordinal gamma.

Assume H3.

Apply H3 to the current goal.

Let r be given.

Assume H3.

Apply H3 to the current goal.

Assume H3: L gamma r.

Assume H4: PNoLe alpha p gamma r.

We will prove ∃delta, ordinal delta ∧ ∃r : set → prop, L delta r ∧ PNoLe beta q delta r.

We use gamma to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is Hc.

We use r to witness the existential quantifier.

Apply andI to the current goal.

An exact proof term for the current goal is H3.

An exact proof term for the current goal is PNoLe_tra beta alpha gamma Hb Ha Hc q p r H2 H4.

∎