proposition: Lemma set1_order_is1 r: order r -> singletonp (substrate r) -> exists x, r = singleton (J x x).
proof: Proof. by move=> or [x xa]; exists x; apply:set1_order_is0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)