proposition: Lemma Exercise2_8d r a A: order r -> inc a (substrate r) -> branched r -> maximal (sub_order (Exercise2_8a_R r a)) A -> ramifiedc (induced_order r A).
proof: Proof. move=> or asr br [As mz]; rewrite (proj2 (sub_osr _)) in As. have aux: forall x, inc x (Exercise2_8a_R r a) -> sub A x-> x = A. move=> x xs xA; apply: mz; apply /sub_gleP; split => //. move: (As) => /Zo_hi [rA _]. move: As; rewrite (Exercise2_8b _ _ or); move => [p1 p2 p3 p4]. split => // [][b] []; rewrite iorder_sr // => bA bm. move: br => [_ br1]. move: (br1 _ (p1 _ bA)) => [c [d [bc bd bcd]]]. Abort. Lemma orsum_wor_aux r g: orsum_ax r g -> worder (order_sum r g) -> (allf g worder). Proof. move=> [or sr alog] [or1 wor]i idg. split; first by apply: alog. move=> x xsr xne. set (y := fun_image x (fun z => (J z i))). have ysr: (sub y (substrate (order_sum r g))). move => t /funI_P [z zx ->]. by rewrite orsum_sr //;apply: disjoint_union_pi1 => //; apply: xsr. have ney: (nonempty y) by apply: funI_setne. move: (wor _ ysr ney) => [z []]; rewrite iorder_sr // => zy zle. move: (zy);move=> /funI_P [t tx zt]. have Px: (inc (P z) x) by rewrite zt; aw. exists (P z); red; rewrite iorder_sr//;last by apply: alog. split => //; move=> s sx; apply /iorder_gleP => //. have py: (inc (J s i) y) by apply /funI_P; ex_tac. move: (iorder_gle1(zle _ py)) => /orsum_gleP [_ _ ]. by rewrite /order_sum_r zt /glt; aw; case; case. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)