proposition: Lemma set1_wor x: worder_on (singleton (J x x)) (singleton x).
proof: Proof. set G := (singleton (J x x)). have Ei: diagonal (singleton x) = G. apply: set1_pr; first by apply/diagonal_pi_P;fprops. by move => z /diagonal_i_P [pa /set1_P]; rewrite - {4} pa => -> <-. have [pa pb] := diagonal_osr (singleton x). have oE: (order G) by rewrite -Ei. have sE: (substrate G = singleton x) by rewrite - Ei pb. split =>//; apply: (worder_prop_rev oE) => y yE [z zy]; ex_tac => t ty. rewrite sE in yE. by rewrite (set1_eq (yE _ zy)) (set1_eq (yE _ ty)); apply/set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)