proposition: Lemma funU_setC A B f (C := (fun_image A f) -s (fun_image (A -s B) f)): fun_image (A -s B) f = (fun_image A f) -s C /\ (finite_set B -> finite_set C).
proof: Proof. have ha: sub (fun_image (A -s B) f) (fun_image A f). by move => t /funI_P[x /setC_P[xoi _]-> ]; apply: funI_i. split; first by rewrite /C setC_K. move => h. have hb: sub C (fun_image B f). move => t /setC_P- [/funI_P [i iA ->] ic]. case: (inc_or_not i B); first by apply: funI_i. by move => ntb; case: ic; apply: funI_i; apply/setC_P. by apply: (sub_finite_set hb); apply: finite_fun_image. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)