proposition: Lemma intersection_singletonP a b c: (a \cap (singleton b) = singleton c) <-> (inc c a /\ c = b).
proof: Proof. split. move=> iis; move:(set1_1 c); rewrite -iis => /setI2_P. by move => [pa] /set1_P. move=> [pa <-]; apply: set1_pr; first by fprops. by move => t /setI2_P [_] /set1_P. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)