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