proposition: Lemma exercise6_1 x g: sgraph g -> ((equivalence g /\ substrate g = x) <-> [/\ domain g = x, range g = x, g \cg ((inverse_graph g) \cg g) = g & sub (diagonal x) g]).
proof: Proof. move=> gg; split. move=> [eg sg]; split => //. - by rewrite (domain_sr eg). - rewrite - sg /substrate; set_extens t => ts; first by fprops. case /setU2_P:ts => // /(domainP gg) [y Jh]; apply/(rangeP gg). exists y; equiv_tac. - set_extens y. move /compg_P => [py [z /compg_pP [u pa /igraph_pP pb pc]]]. have J4: inc (J u z) g by equiv_tac. have J5: inc (J (P y) z) g by equiv_tac. have: inc (J (P y) (Q y)) g by equiv_tac. by rewrite py. move=> yg. have py: pairp y by apply: gg. have yv:J (P y) (Q y) = y by aw. rewrite - py; apply /compg_pP; exists (P y); last by ue. apply /compg_pP; exists (Q y); [| apply/igraph_pP]; ue. - move => t /diagonal_i_P [pt Pt PQt]. by rewrite -pt -PQt; rewrite - sg in Pt; equiv_tac. move=> [dg rg cg si]. have sg: (substrate g = x) by rewrite /substrate dg rg; apply: setU2_id. split=>//. have p1: forall u, inc u x -> inc (J u u) g. by move=> u ux; apply: si; apply /diagonal_pi_P. have p2: symmetricp g. move=> a b ab; red in ab. have Jag: (inc (J a a) g) by apply: p1; rewrite -dg; aw; ex_tac. have Jbg: (inc (J b b) g) by apply: p1; rewrite -rg; aw; ex_tac. rewrite -cg; apply /compg_pP; ex_tac; apply /compg_pP; ex_tac. by apply /igraph_pP. have p3: transitivep g. move => a b c ab bc; rewrite -cg; apply /compg_pP. exists a => //; apply /compg_pP; exists b => //. by apply: p1; rewrite - sg; substr_tac. by apply/igraph_pP; apply p2. by apply:symmetric_transitive_equivalence. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)