proposition: Lemma isDiaP s : isDia_spec s (isDia s).
proof: Proof. move: s => [ [|?|? ?|?|?] [|]] /=; try constructor. exact: isDia_true. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)