proposition: Lemma supp_mon L1 L2 s : L1 `<=` L2 -> L1 |> s -> L2 |> s.
proof: Proof. move/subP => sub. case: s. elim => //= [|p|s IHs t IHt|s IHs|s IHs] [|]; solve [exact: sub| rewrite -?(rwP orP,rwP andP); intuition]. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)