proposition: Lemma subset_trans A B C : A \subset B -> B \subset C -> A \subset C.
proof: Proof. by move/subsetP=> sAB /subsetP=> sBC; apply/subsetP=> x /sAB; apply: sBC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)