proposition: Lemma eq_proper_r A B : A =i B -> (@proper T)^~ (mem A) =1 (@proper T)^~ (mem B).
proof: Proof. move=> eAB [C]; congr (_ && _); first exact: (eq_subset_r eAB). by rewrite (eq_subset eAB). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)