proposition: Lemma properD A B C : (A \proper B :\: C) -> (A \proper B) && [disjoint A & C].
proof: Proof. by rewrite setDE disjoints_subset => /properI/andP[-> /proper_sub]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)