proposition: Lemma lift0_perm_eq0 s i : (lift0_perm s i == 0) = (i == 0).
proof: Proof. by rewrite (canF_eq (lift0_permK s)) lift0_perm0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg countalg finalg zmodp)