proposition: Lemma ns_extensions_prop6: inc ((ordinal rB) +o (ordinal rA)) ns_extensions_ord.
proof: Proof. move:ns_extensions_prop4 => [pa pb]. apply/funI_P; ex_tac. have oa := proj1 wor1; have ob := proj1 wor2. apply:(orsum_invariant5 ob oa pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)