proposition: Lemma subset_gen A : A \subset <<A>>.
proof: Proof. rewrite [@generated]unlock; exact/bigcapsP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)