proposition: Lemma fproperD2l C A B : A `<=` C -> B `<=` C -> (C `\` B `<` C `\` A) = (A `<` B).
proof: Proof. move=> sAC sBC; apply/idP/idP; last exact: fsetDpS. by move=> /(@fsetDpS C); rewrite !fsetDK //; apply; apply: fsubsetDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)