proposition: Lemma Zo_i x (p:property) y: inc y x -> p y -> inc y (Zo x p).
proof: Proof. rewrite /Zo => -[a Roa]; rewrite -{1} Roa => py. by apply/ IM_P; exists (Zorec_c (f:= (fun a : x => p (Ro a))) py). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)