proposition: Lemma subsetUr A B : B \subset A :|: B.
proof: Proof. by apply/subsetP=> x; rewrite inE orbC => ->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)