proposition: Lemma icor_correspondence m: correspondence m -> correspondence (inverse_fun m).
proof: Proof. move => [_ pb]; apply: corresp_create => x/igraphP [px pg]. by move /setXp_P: (pb _ pg) => [pc pd]; apply: setX_i. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)