proposition: Lemma properP A B : reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B).
proof: Proof. by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)