proposition: Lemma ImageIm A B C (f1 : B -> C) (f2 : A -> B) (X : Pred A) : Image f1 (Image f2 X) =p Image (f1 \o f2) X.
proof: Proof. move=>x; split; first by case=>_ -> [x' ->] H; exists x'. by case=>a -> H; exists (f2 a)=>//; exists a. Qed.
imports: Coq(ssreflect ssrbool ssrfun Setoid) mathcomp(ssrnat seq eqtype) pcm(options)