proposition: Lemma inj_strictf_ffun (p q : nat) (f: {ffun 'I_p -> 'I_q}) : strictf f -> injective f.
proof: Proof. by move=> h; apply: inj_strictf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor