proposition: Lemma image_smaller1 f x: function f -> (Vfs f x) <=cc x.
proof: Proof. move => pa. move: (@subsetI2l x (source f)) (@subsetI2r x (source f)) => a1 a2. have ->: Vfs f x = Vfs f (x \cap (source f)). set_extens t => /dirim_P [u p1 p2]; apply /dirim_P; exists u => //. apply /setI2_P;split => //; Wtac. by apply: a1. move: (restriction1_fs pa a2) (sub_smaller a1) => sjb le1. move: (image_smaller (proj1 sjb)). rewrite (surjective_pr0 sjb) /restriction1; aw => le2; apply:cleT le2 le1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)