proposition: Lemma in_fset1 a' a : a \in [fset a'] = (a == a').
proof: Proof. by rewrite !in_fset_ orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)