proposition: Lemma prelift_reduce s : prelift (reduce s) = prelift s.
proof: Proof. rewrite /reduce; set S := foldr _ _ _; set rD := filter _ _. have ->: prelift rD = prelift S; rewrite {}/rD. elim: S => [//|[k x] S IHS] /=; have [->|nz_k] := eqVneq k 0. by rewrite /= prelift_cons scale0r add0r. by rewrite !prelift_cons IHS. rewrite {}/S; elim: s => [//|[k x] s IHs]. by rewrite prelift_cons /= prelift_augment IHs. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop order generic_quotient) mathcomp(ssralg ssrnum ssrint)