proposition: Lemma eq_subset_r A B : A =i B -> (@subset T)^~ (mem A) =1 (@subset T)^~ (mem B).
proof: Proof. move=> eqAB [C]; rewrite !unlock; congr (_ == 0). by apply: eq_card => x; rewrite !inE /= eqAB. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)