proposition: Lemma set1_ordinal r: order r -> singletonp (substrate r) -> ordinal r = \1o.
proof: Proof. move=> ox sx; move: (set1_order_is1 ox sx) => [y ->]; exact:ordinal1_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)