proposition: Lemma codom_comp T U V (f : U -> T) (g : V -> U) : codom (f \o g) <--> f @: (codom g).
proof: Proof. by rewrite -imsetT imset_comp imsetT. Qed.
imports: mathcomp.ssreflect.ssreflect Classes.RelationClasses Classes.Morphisms List Tactics mathcomp(ssrfun ssrbool ssrnat seq)