proposition: Lemma isum_q2 I: sub I E -> worder (ipartial_order I).
proof: Proof. move: fprop => [qa qb ofs] seN. move:(isum_q1 seN) => h. apply: orsum_wor; hnf; aw; trivial => x xe; rewrite LgV//. by apply: ordinal_o_wor; apply: ofs; rewrite qb; apply: seN. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)