proposition: Lemma isum_q4 I: sub I E -> orsum_ax (io I)(Lg I (fun z => ordinal_o (Vg f z))).
proof: Proof. move:fprop => [qa qb ofs] seN. move:(isum_q1 seN) => [[or _ ] sr]. split => //; hnf; aw; trivial; move => t tE; rewrite LgV//;rewrite - qb in seN. exact: (proj1 (ordinal_o_wor (ofs _ (seN _ tE)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)