proposition: Lemma maxn_fsetD n m (A : {fset nat}) : maxn n m \notin A `\` [fset n; m].
proof: Proof. by rewrite inE negb_and negbK maxn_fset2. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries)