proposition: Lemma diagonal_equivalence x: equivalence_on (diagonal x) x.
proof: Proof. rewrite -diagonal_graph_on; split; last by rewrite graph_on_sr // => t tx. apply: equivalence_from_rel;split. by move=> a b /= [ax] <-. by move=> a b c [au ab] [bu bc]; split =>//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)