proposition: Lemma Exercise2_6d a: inc a (source f) -> inc (chainx a) bigS.
proof: Proof. move => asf. move: (Exercise2_6b asf) =>ne; move: (ne) => [u ub]. apply: Zo_i. apply /setP_P; move=> t td; move: (setI_hi td ub). by move: ub => /Zo_P [] /Zo_P [] /setP_P usr _ _ tu ; apply: usr. split. move=> x xc; apply: setI_i => //. move=> y yb; move: (setI_hi xc yb). by move: yb => /Zo_P [] /Zo_P [] /setP_P _ [p _] _ tu; apply: p. move=> N x Nca neN leN. apply: setI_i => // y yb; move: (yb) => /Zo_P [yc ay]. move: yc => /Zo_P [_ [_ p]]; apply: (p N x) => //. move=> t tN ; exact: (setI_hi (Nca _ tN) yb). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)