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