proposition: Lemma msetB1P x A b : reflect ((x = b -> A x > 1) /\ x \in A) (x \in A `\ b).
proof: Proof. rewrite !inE. apply: (iffP andP); first by move=> [/implyP Ax ->]; split => // /eqP. by move=> [Ax ->]; split => //; apply/implyP => /eqP. Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop tuple) finmap