proposition: Lemma same_codomP m n (f g : {ffun 'I_m -> 'I_n}) : reflect (same_codom f g) (same_codomb f g).
proof: Proof. apply: (iffP forallP) => h x. - by rewrite (eqP (h x)). by rewrite (h x). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor