proposition: Lemma strictf_uniq : forall m n (f g: {ffun 'I_m -> 'I_n}), strictf f -> strictf g -> same_codom f g -> f = g.
proof: Proof. clear A B Z R k l. elim => [ | m hi] n f g hf hg hsame; apply/ffunP; first by case. move/forallP : (hf) => hf1. move/forallP : (hg) => hg1. rewrite [m.+1]/(1 + m)%nat => x. case: (ltngtP (f 0) (g 0)) => h. - have h1 : f 0 \in codom g by rewrite -hsame codom_f. have [x' heq] : { x' | f 0 = g x'} by exists (iinv h1); rewrite f_iinv. move: h; rewrite heq. move/forallP : (hg1 x') => hg'. by rewrite -(eqP (hg' 0)) ltn0. - have h1 : g 0 \in codom f by rewrite hsame codom_f. have [x' heq] : { x' | g 0 = f x'} by exists (iinv h1); rewrite f_iinv. move: h; rewrite heq. move/forallP : (hf1 x') => hf'. by rewrite -(eqP (hf' 0)) ltn0. case: (splitP x) => y. - rewrite [y]ord1 => hy. have {x hy}-> : x = 0 by apply/ord_inj. by apply/ord_inj. move => hy. have {x hy}-> : x = lift 0 y by apply/ord_inj. set f' := finfun (fun x => f (lift 0 x)). set g' := finfun (fun x => g (lift 0 x)). have hsame' : forall x, (x \in codom f') = (x \in codom g'). - move => z. apply/imageP/imageP. + case => /= a _; rewrite ffunE => hz. have : z \in codom g by rewrite -hsame hz codom_f. case/imageP; rewrite [m.+1]/(1 + m)%nat => x' _. case: (splitP x') => j. * rewrite [j]ord1 => hx'. have {x' hx'}-> : x' = 0 by apply/ord_inj. move => h'. have : f (lift 0 a) = f 0 by apply/ord_inj; rewrite -hz h h'. by move/(inj_strictf hf). move => hx'. have {x' hx'}-> : x' = lift 0 j by apply/ord_inj. move => hz'. by exists j => //; rewrite ffunE. case => /= a _; rewrite ffunE => hz. have : z \in codom f by rewrite hsame hz codom_f. case/imageP; rewrite [m.+1]/(1 + m)%nat => x' _. case: (splitP x') => j. * rewrite [j]ord1 => hx'. have {x' hx'}-> : x' = 0 by apply/ord_inj. move => h'. have : g (lift 0 a) = g 0 by apply/ord_inj; rewrite -hz -h h'. by move/(inj_strictf hg). move => hx'. have {x' hx'}-> : x' = lift 0 j by apply/ord_inj. move => hz'. by exists j => //; rewrite ffunE. move/ffunP : (hi n f' g' (strictf_lift hf) (strictf_lift hg) hsame') => heq. by move: (heq y); rewrite !ffunE => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor