proposition: Lemma diagonal_length E: nonempty E -> the_order_length (diagonal E) = \1c.
proof: Proof. move => [u uE]. move: (diagonal_osr E) =>[or sr]. have usE: inc u (substrate (diagonal E)) by ue. apply:(the_max_card_on_set_prop2 NS1); split. exists (singleton u); last by rewrite cardinal_set1. exact:(torder_set1 or usE). move => x /total_subordersP [xE [ot ti]]; apply:cardinal_small_set. move: (iorder_sr or xE) => si a b ax bx; move: (ti a b); rewrite si => h. by case:(h ax bx) => /iorder_gle1 /diagonal_pi_P []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)