proposition: Lemma exercise6_2 g: sgraph g -> g \cg ( (inverse_graph g) \cg g) = g -> [/\ equivalence ((inverse_graph g) \cg g), substrate ((inverse_graph g) \cg g) = domain g, equivalence (g \cg (inverse_graph g)) & substrate (g \cg (inverse_graph g)) = range g].
proof: Proof. move=> gg cg. have gig:sgraph (inverse_graph g) by apply: igraph_graph. have gcigg:sgraph ((inverse_graph g) \cg g) by apply: compg_graph. have gcgig: sgraph (g \cg (inverse_graph g)) by apply: compg_graph. have t3:forall x y z t, related g x y -> related g z y -> related g z t -> related g x t. move=> x y z t xy zy zt; rewrite -cg; apply/compg_pP. by exists z=>//;apply/compg_pP;exists y => //;apply /igraph_pP. have s1: substrate ((inverse_graph g) \cg g) = domain g. set_extens x. case /(substrate_P gcigg) => [] [y /compg_pP [z J1] /igraph_pP J2]; ex_tac. move/(domainP gg) => [y Jg]. have Jxx: (inc (J x x) ((inverse_graph g) \cg g)). by apply/compg_pP; ex_tac; apply /igraph_pP. apply: (arg1_sr Jxx). have s2:substrate (g \cg (inverse_graph g)) = range g. set_extens x. case/(substrate_P gcgig)=> [][y /compg_pP [z /igraph_pP J1 J2]]; ex_tac. move/(rangeP gg) => [y Jg]. have Jxx: (inc (J x x) (g \cg (inverse_graph g))). by apply/compg_pP; ex_tac; apply /igraph_pP. apply: (arg1_sr Jxx). split => //; rewrite equivalence_pr; split; try rewrite compg_inverse igraph_involutive //. by rewrite - compgA cg. by rewrite compgA in cg; by rewrite compgA cg. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)