proposition: Lemma oprod1r a: ordinalp a -> a *o \1o = a.
proof: Proof. move=> ox; rewrite (oprod_rec_def ox OS1). have h: forall t, inc t a -> t = a *o \0o +o t. move => t tx; rewrite oprod0r osum0l //; exact: (Os_ordinal ox tx). set_extens t. by move/funI_P => [z /setX_P [p1 p2 /set1_P ->] ->]; rewrite - h. move => tx; apply /funI_P; exists (J t \0o); last by aw; apply h. by apply:setXp_i; fprops; apply/set1_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)