proposition: Lemma weightS L : (0 < weight L) -> ~~ literalC L.
proof: Proof. rewrite lt0n. apply: contra => /allP H. apply/eqP. by have/fsum_const : {in L, const 0 s_weight} by move => x /H /sweight_lit. Qed.
imports: mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert)