proposition: Lemma NS_quo a b: natp a -> natp (a %/c b).
proof: Proof. rewrite cquoE /cquo_internal /least_ordinal => /olt_omegaP aN. set E := Zo _ _. have nsE x: inc x E -> natp x. move => /Zo_S /(oleP (proj31_1 aN)) xa; apply/olt_omegaP; apply: (ole_ltT xa aN). have osE: ordinal_set E by move => t /nsE /OS_nat. case: (emptyset_dichot E) => Enz; first by rewrite Enz setI_0; fprops. exact: (nsE _ (ordinal_setI Enz osE)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)