proposition: Lemma fun_image_smaller a f: (fun_image a f) <=cc a.
proof: Proof. have sjb: (surjection (Lf f a (fun_image a f))). apply: lf_surjective; first by move=> t ta; apply /funI_P; ex_tac. by move=> y /funI_P. by move: (image_smaller (proj1 sjb)); rewrite (surjective_pr0 sjb); aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)