proposition: Lemma subsetP A B : reflect {subset A <= B} (A \subset B).
proof: Proof. rewrite unlock; apply: (iffP (pred0P _)) => [AB0 x | sAB x /=]. by apply/implyP; apply/idPn; rewrite negb_imply andbC [_ && _]AB0. by rewrite andbC -negb_imply; apply/negbF/implyP; apply: sAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)