proposition: Lemma sub_proper_trans A B C : A \subset B -> B \proper C -> A \proper C.
proof: Proof. move=> sAB /properP[sBC [x Cx nBx]]; rewrite properE (subset_trans sAB) //. by apply/subsetPn; exists x => //; apply: contra nBx; apply: subsetP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)