proposition: Lemma pAR_pEU (p q : X -> Prop) (w : X) : pEU (PredC p) (PredC q) w -> ~ pAR p q w.
proof: Proof. case => pi [pi1 pi2 pi3]. move/(_ pi pi1 pi2) => pi4. case: pi3 => n n1 n2. case: (pi4 n) => [[m m1 m2]|]. - exact: n1 (m) _ _. - exact: n2. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(all_ssreflect) CompDecModal.libs(edone bcase fset base modular_hilbert sltype)