proposition: Lemma subset_eqP A B : reflect (A =i B) ((A \subset B) && (B \subset A)).
proof: Proof. apply: (iffP andP) => [[sAB sBA] x| eqAB]; last by rewrite !eq_subxx. by apply/idP/idP; apply: subsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)