proposition: Lemma proper_trans A B C : A \proper B -> B \proper C -> A \proper C.
proof: Proof. case/properP=> sAB [x Bx nAx] /properP[sBC [y Cy nBy]]. rewrite properE (subset_trans sAB) //=; apply/subsetPn; exists y => //. by apply: contra nBy; apply: subsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)