proposition: Lemma osum_unit1 r g I: orsum_ax r g -> sub I (domain g) -> (forall i, inc i ((domain g) -s I) -> Vg g i = emptyset) -> (order_sum r g) \Is (order_sum (induced_order r I) (restr g I)).
proof: Proof. move => oa sI alz; move: (oa) => [or sr alo]. have dr: (domain (restr g I)) = I by aw. have sI1: sub I (substrate r) by ue. have oa': orsum_ax (induced_order r I) (restr g I). have [pa pb]:= (iorder_osr or sI1). hnf; rewrite pb;split => //; hnf;rewrite dr. move=> i id; rewrite LgV //; apply: (alo _ (sI _ id)). have o1: order (order_sum r g) by fprops. have o2: order (order_sum (induced_order r I) (restr g I)) by fprops. set E := substrate (order_sum r g). set F := substrate (order_sum (induced_order r I) (restr g I)). have EF: E = F. set_extens z; rewrite /E/F !orsum_sr //. move => zs; move: (du_index_pr1 zs) => [Qd Pd <-]. case: (inc_or_not (Q z) I) => aux. by apply: disjointU_pi => //; aw; trivial; rewrite !LgV//; aw. have Qx: inc (Q z) ((domain g) -s I) by fprops. have Ve := (alz _ Qx). by move:Pd;rewrite Ve (proj2 set0_wor) => /in_set0. move => zs; move: (du_index_pr1 zs) => [Qd Pd <-]. rewrite dr in Qd; rewrite LgV // in Pd. have qq: inc (Q z) (domain g) by apply:sI. by apply: disjointU_pi; aw; trivial;rewrite LgV. exists (identity E). hnf; rewrite/bijection_prop identity_s identity_t; split => //. split => //;apply: identity_fb. have a1: forall x, inc x F -> inc (Q x) I. move=> x; rewrite /F orsum_sr // => xs; move: (du_index_pr1 xs)=> [aux _]; ue. hnf; aw; move=> x y xE yE; rewrite idV //. rewrite orsum_gleP orsum_gleP. have <-: E = (sum_of_substrates g) by rewrite /E orsum_sr. have <-: F = (sum_of_substrates (restr g I)) by rewrite /F orsum_sr. rewrite idV ///order_sum_r -EF /glt. have aux: (gle (induced_order r I) (Q x) (Q y) <-> (gle r (Q x) (Q y))). rewrite/gle/related/induced_order; split. by move /setI2_P => []. move=> h; apply /setI2_P; split => //; apply: setXp_i; apply: a1; ue. have ->: Vg (restr g I) (Q x) = (Vg g (Q x)). rewrite LgV //;apply: a1; ue. by split; move => [pa pb pc];split => //; case: pc => //; try (by right); move => [/aux pd pe];left. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)