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