proposition: Lemma properU A B C : (B :|: C \proper A) -> (B \proper A) && (C \proper A).
proof: Proof. move=> pUA; apply/andP. by split; apply: sub_proper_trans pUA; rewrite (subsetUr, subsetUl). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)