proposition: Lemma strictf_lift m n (f: {ffun 'I_m.+1 -> 'I_n}) : strictf f -> strictf (finfun (fun x => f (lift 0 x))).
proof: Proof. move/forallP => hf. apply/forallP => /= x. apply/forallP => /= y. rewrite !ffunE. move/forallP : (hf (lift 0 x)) => hf'. by rewrite -(eqP (hf' (lift 0 y))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype perm choice finfun) mathcomp(matrix bigop zmodp mxalgebra fingroup) minor