proposition: Lemma properIset A B C : (B \proper A) || (C \proper A) -> (B :&: C \proper A).
proof: Proof. by case/orP; apply: sub_proper_trans; rewrite (subsetIl, subsetIr). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)