proposition: Lemma tuto_mem_seq1 : forall x y, (x \in [:: y]) = (x == y).
proof: Proof. by move=> x y; rewrite in_cons orbF. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)