proposition: Lemma ns_extensions_prop5: inc ((ordinal rA) +o (ordinal rB)) ns_extensions_ord.
proof: Proof. move:ns_extensions_prop3=> ha; apply/funI_P; ex_tac. have oa := proj1 wor1; have ob := proj1 wor2. apply:(orsum_invariant5 oa ob); apply: orderIR. exact: (proj1 (orsum2_wor oa ob)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)