proposition: Lemma inj_lift m n (f : 'I_n -> 'I_m) : injective f -> injective (lift_pred f).
proof: Proof. rewrite /lift_pred => hf x y; rewrite !split1. have [/= j ->|->] := unliftP; last by have [|-> //] := unliftP. by have [/= i -> /lift_inj/hf ->|] := unliftP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)