proposition: Lemma lift0_perm0 s : lift0_perm s 0 = 0.
proof: Proof. exact: lift_perm_id. 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)