proposition: Lemma foldr_maxnE m u s : (foldr maxn m s <= u = (m <= u) && (all (fun t => t <= u) s))%nat.
proof: Proof. elim: s => [| ? ? IH] /=; by [rewrite andbT | rewrite geq_max IH andbCA]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist