proposition: Lemma iso_graph_inj2 g a b c: inc g iso_graphs -> inc (J c a) g -> inc (J c b) g -> a = b.
proof: Proof. move =>/Zo_P[/setP_P h [pa pb pc pd]] i1 i2. move:(proj1 wor1) (proj1 wor2) => or1 or2. move: (h _ i1) (h _ i2) => /setXp_P [csr asr] /setXp_P [_ bsr]. have cc: gle r1 c c by order_tac. move/(pd _ _ _ _ i1 i2): (cc) => l1. move/(pd _ _ _ _ i2 i1): cc => l2. order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)