proposition: Lemma fproperU A B C : (B `|` C `<` A) -> (B `<` A) && (C `<` A).
proof: Proof. move=> pUA; apply/andP. by split; apply: fsub_proper_trans pUA; rewrite (fsubsetUr, fsubsetUl). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)