proposition: Lemma nsub_contra C D : C \in S -> D \in S -> ~~ (C `<=` D) -> prv ([af C] ---> [af D] ---> fF).
proof: Proof. Proof using sub_S. move => /(subP sub_S). rewrite inE powersetE. case/and3P => sub _ _. move/(subP sub_S). rewrite inE. case/and3P => _ _ /allP maxD. case/subPn. case => s [|]; move => inC ninD; move: (maxD s); rewrite (negbTE ninD) ?orbF /=; rewrite -> (bigAE _ inC); move: inC => /(subP sub) => inF; rewrite (flip_drop_sign inF) => inD; rule axC; (rewrite -> bigAE; last exact: inD); [done| by rule axC]. Qed.
imports: Relations mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert) CompDecModal.PDL(PDL_def demo)