proposition: Lemma equivalence_relation_bourbaki_ex5 A E (r := (fun x y => (inc x (E -s A) /\ (x = y) \/ (inc x A /\ inc y A)))): sub A E -> equivalence_on (graph_on r E) E.
proof: Proof. move => sa; split; last first. apply: graph_on_sr; move => a ae. by case: (inc_or_not a A) => h; [right | left]; split => //; apply /setC_P. apply: equivalence_from_rel; split. move=> x y; case=> [] [pa pb]; [left | right ]; split => //; ue. move => y x z [] [pa pb]; first by rewrite pb. move => h;right; case:h => [] [qa qb]; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)