proposition: Lemma Exercise2_6b a: inc a (source f) -> nonempty (Zo bigS (inc a)).
proof: Proof. move=> asf;exists (substrate r); apply: Zo_i;[ apply: Exercise2_6a| ue]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)