proposition: Lemma bij_eqLR (aT rT : finType) (f : bij aT rT) x y : (f x == y) = (x == f^-1 y).
proof: Proof. by rewrite -{1}[y](bijK' f) bij_eq. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries)