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