proposition: Lemma tuto_minsetp : forall P A, minset P A -> P A.
proof: Proof. by move=> P A; case/minsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finset)