proposition: Lemma sweight_lit s : s_weight s = 0 <-> literal s.
proof: Proof. case: s => [[|p|s t|s|s t|s t] [|]] //. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)