proposition: Lemma fsetU1_fun_can (T : choiceType) (A B : {fset T}) (x y : T) (f : A -> B) (g : B -> A) : x \notin A -> y \notin B -> cancel f g -> cancel (fsetU1_fun f x y) (fsetU1_fun g y x).
proof: Proof. move => Hx Hy can_f a. rewrite {2}/fsetU1_fun. case: fset1UE => [/=|[D Ha]]. - rewrite /fsetU1_fun. case: fset1UE => //=. + move => _ E. apply: val_inj => /=. by rewrite E. + rewrite eqxx. by case. - rewrite /fsetU1_fun /=. case: fset1UE. + move => E. by rewrite -E (fsvalP _) in Hy. + case => A1 A2. apply: val_inj => //=. rewrite (_ : [`A2] = (f.[Ha])%fmap) ?can_f //. exact: val_inj. Qed.
imports: mathcomp(all_ssreflect) Coq(Relations.Relation_Definitions) GraphTheory(edone preliminaries) GraphTheory(bij)