proposition: Lemma osum_unit2 r g I: worder_on r (domain g) -> ordinal_fam g -> sub I (domain g) -> (forall i, inc i ((domain g) -s I) -> Vg g i = \0o) -> osum r g = osum (induced_order r I) (restr g I).
proof: Proof. move => [wor sr] odf sj alne. have or:= proj1 wor. rewrite /osum/order_sum; apply: ordinal_o_isu1. apply:orsum_wor; [saw | hnf; aw => i idg;rewrite LgcV ; fprops]. apply: orsum_wor. split; first by apply: induced_wor => //; ue. rewrite iorder_sr //; aw; trivial; ue. hnf; aw => i idg; rewrite !LgV// //; aww. rewrite /Lgcomp. set g1:= (Lg (domain g) (fun z => ordinal_o (Vg g z))). set g2:= Lg _ _. have ->: g2 = (restr g1 I). by rewrite /g1 /g2; aw; apply: Lg_exten => x xd; rewrite !LgV//; apply: sj. have dg1: domain g1 = domain g by rewrite /g1; aw. apply: osum_unit1. split; [exact | ue | ]. by hnf; rewrite dg1; move=> i idg; rewrite /g1 LgV//; apply: ordinal_o_or. ue. rewrite dg1; move=> i ic; rewrite /g1 LgV//. by rewrite (alne _ ic) ordinal_o_set0. by move: ic => /setC_P [ok _]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)