proposition: Lemma fsetDpS C A B : B `<=` C -> A `<` B -> C `\` B `<` C `\` A.
proof: Proof. move=> subBC subAB; rewrite fproperEneq fsetDS 1?fproper_sub// andbT. apply/negP => /eqP /(congr1 (fsetD C)); rewrite !fsetDK // => [eqAB//|]. by rewrite eqAB (negPf (fproper_irrefl _)) in subAB. by apply: fsubset_trans subBC; apply: fproper_sub. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)