proposition: Lemma subxx_hint (mA : mem_pred T) : subset mA mA.
proof: Proof. by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)