proposition: Lemma lift_pred0 n k (f: 'I_k -> 'I_n) : lift_pred f 0 = 0.
proof: Proof. by rewrite /lift_pred; case: splitP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)