proposition: Lemma supp_aux C : C \in powerset F -> mprv ([af C] ---> \or_(D <- base LF C) [af D]).
proof: Proof. Proof using ssub_F ssub decompP. move: C. apply: @nat_size_ind _ _ (@weight _) _ => C IH inU. case: (posnP (weight C)) => [/weight0 lC |/weightS wC]. - apply (bigOI xaf). by rewrite !inE suppxx; bcase. - case/allPn : wC => s inC nL. case: (decompP s) => [|S S1 S2 S3 S4]; first by rewrite (negbTE nL). rewrite -{1}(fsetUD1 inC). rewrite -> andU, bigA1, S4. rewrite -> bigODr. apply: bigOE => D inCs. rewrite <- andU. rewrite -> IH. + apply: bigOE => L'. rewrite !inE -andbA => /and3P [D1 D2 D3]. apply: (bigOI xaf). rewrite !inE D1 D2 /=. move: D3. rewrite suppCU => /andP [D3]. apply: suppCD. rewrite /suppC all_fset1. exact: S3 D3. + apply: fsum_replace; rewrite ?fsub1 // fsum1. exact: S2. + rewrite powersetU [_ `\` _ \in _](sub_power _ inU) // andbT. rewrite powersetE. apply: sub_trans (S1 _ inCs) _. apply ssub_F. rewrite powersetE in inU. exact: (subP inU). Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert)