proposition: Lemma forall_inPn (T : finType) (p q : pred T) : reflect (exists2 x, p x & ~~ q x) (~~ [forall (x | p x), q x]).
proof: Proof. rewrite negb_forall (eq_existsb (P2 := fun x => p x && ~~ q x)) => [|x]. exact: exists_inP. exact: negb_imply. Qed.
imports: mathcomp(all_ssreflect) Relations CompDecModal.libs(edone bcase)