proposition: Lemma Exercise2_6c a: inc a (source f) -> inc a (chainx a).
proof: Proof. move=> asf; apply: setI_i; first by apply: Exercise2_6b =>//. by move=> y /Zo_hi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)