proposition: Lemma tuto_set1P : forall x a, reflect (x = a) (x \in [set a]).
proof: Proof. move=> x a; rewrite inE; exact: eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)