proposition: Lemma properI A B C : (A \proper B :&: C) -> (A \proper B) && (A \proper C).
proof: Proof. move=> pAI; apply/andP. by split; apply: (proper_sub_trans pAI); rewrite (subsetIl, subsetIr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)