proposition: Lemma properD1 X x : x \in X -> X `\` [fset x] `<` X.
proof: Proof. move => H. rewrite /proper fsubDl /=. apply/subPn. by exists x; rewrite ?in_fset; bcase. Qed.
imports: Recdef mathcomp(all_ssreflect) CompDecModal.libs(edone bcase base)