proposition: Lemma in_imset {U T} (f : U -> T) (S : set U) (x : T) : (f @: S) x -> exists y, x = f y.
proof: Proof. move => [y [H1 H2]]; eauto. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)