proposition: Lemma graph_on_exten (p q: relation) E: (forall x y, inc x E -> inc y E -> (p x y <-> q x y)) -> graph_on p E = graph_on q E.
proof: Proof. move => hyp. by set_extens t;move/Zo_P => [pa pb]; move/setX_P: (pa) => [_ qa qb]; apply: (Zo_i pa); apply/hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)