proposition: Lemma ns_extensions_prop3: inc (order_sum2 rA rB) ns_extensions.
proof: Proof. apply/ns_extensions_prop1. move: wor1 wor2 =>[wo1 sr1][wo2 sr2]. move: (orsum2_wor wo1 wo2) => wor3. move: (orsum2_sr (proj1 wo1) (proj1 wo2)) ; rewrite sr1 sr2 -/C => h. split => //. move => t /Zo_P [/setX_P[qa qb qc] qd]; rewrite - qa; apply orsum2_gleP. rewrite sr1 sr2; split => //; case: qd => qe; in_TP4. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)