proposition: Lemma sub_gen A B : A \subset B -> A \subset <<B>>.
proof: Proof. by move/subset_trans=> -> //; apply: subset_gen. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)