proposition: Lemma setDSS A B C D : A \subset C -> D \subset B -> A :\: B \subset C :\: D.
proof: Proof. by move=> /(setSD B) /subset_trans sAC /(setDS C) /sAC. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)