proposition: Lemma fset2_maxn_neq n m x : x \notin [fset n; m] -> x != maxn n m.
proof: Proof. apply: contraNneq => ->. exact: maxn_fset2. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries)