proposition: Lemma tuto_eqEsubset : forall A B, (A == B) = (A \subset B) && (B \subset A).
proof: Proof. by move=> A B; apply/eqP/subset_eqP; move/setP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)