proposition: Lemma bij_same A B (f : A -> B) (f_inv : B -> A) (i : bij A B) : f =1 i -> f_inv =1 i^-1 -> bij A B.
proof: Proof. move => Hf Hf'. exists f f_inv; abstract (move => x; by rewrite Hf Hf' ?bijK ?bijK'). Defined.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)