#n; napply le_S_S; napply le_O_n.
nqed.
-ndefinition Nat_: nat → qpowerclass NAT.
- #n; napply mk_qpowerclass
+ndefinition Nat_: nat → ext_powerclass NAT.
+ #n; napply mk_ext_powerclass
[ napply {m | m < n}
| #x; #x'; #H; nrewrite < H; napply mk_iff; #K; nassumption (* refl non va *) ]
nqed.