proposition: Lemma mem_same_codom (f g: {ffun 'I_k -> 'I_l}) : same_codom f g -> forall x, f x \in codom g.
proof: Proof. by move => h x; rewrite -h codom_f. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor