proposition: Lemma igraph_identity_g x: inverse_graph (identity_g x) = identity_g x.
proof: Proof. rewrite/inverse_graph identity_r identity_d - diagonal_is_identity. set_extens z;move /Zo_P => [pa pb]; apply: Zo_i => //. by move/Zo_hi: pb; aw. by rewrite -pb;apply/diagonal_pi_P;split => //; move /setX_P: pa => [_]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)