proposition: Lemma strict_fromP (f: {ffun 'I_k -> 'I_l}) (hf: injective f): strictf (strict_from hf) /\ same_codom f (strict_from hf).
proof: Proof. split. - apply/forallP => x. apply/forallP => y. have hsorted : sorted ltn (map val (enum (codom f))) by apply: sorted_enum. apply/eqP. rewrite !ffunE /enum_val -!tool_nth. apply/idP/idP => [ hxy | ]. + apply: sorted_ordered_nth => //. * by rewrite size_map cast0 ltn_ord. by rewrite size_map cast0 ltn_ord. apply: sorted_ordered_nth_gen => //=. + by rewrite size_map cast0 -(cast1 hf) ltn_ord. by rewrite size_map cast0 -(cast1 hf) ltn_ord. have h1 : enum (codom f) =i codom f by move => y; rewrite mem_enum. move => y. apply/imageP/imageP. - case => x hx hy. have hy' : y \in (enum (codom f)) by rewrite h1 hy codom_f. have hi : index y (enum (codom f)) < #|codom f| by rewrite -cast0 index_mem. have hi' : index y (enum (codom f)) < k by move: hi; rewrite -cast1. exists (Ordinal hi') => //. by rewrite !ffunE /enum_val /= nth_index. case => /= x hx. rewrite !ffunE => hy. have : (y \in codom f) by rewrite hy; apply/enum_valP. case/imageP => x' _ hx'. by exists 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