proposition: Lemma subset_catr s s' : s \subset s' ++ s.
proof: Proof. by apply/subsetP => x xins; rewrite mem_cat xins orbT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(path div)