1 lapply (nta_ntas … H) -H #H
2 elim (ntas_inv_appl_sn … H) -H * #n #p #W #U #U0 #Hn #Ha #HVW #HTU #HU #HUX #HX
3 [ elim (eq_or_gt n) #H destruct
4 [ <minus_n_O in HU; #HU -Hn
5 /4 width=8 by ntas_inv_nta, ex6_4_intro, or_introl/
6 | lapply (le_to_le_to_eq … Hn H) -Hn -H #H destruct
9 @(ex6_5_intro … Ha … HUX HX) -Ha -X
10 [2,4: /2 width=2 by ntas_inv_nta/