proposition: Lemma ordinal1_pr x: ordinal (singleton (J x x)) = \1o.
proof: Proof. have [p1 p2]:= (set1_wor x). apply: (ordinal_o_isu2 p1 OS1); apply: set1_order_is2; fprops. by rewrite p2; exists x. by rewrite ordinal_o_sr; exists emptyset. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)