proposition: Lemma oprod1l a: ordinalp a -> \1o *o a = a.
proof: Proof. move: a; apply:least_ordinal2' => c oc H. rewrite (oprod_rec_def OS1 oc); set_extens t. move/funI_P => [z /setX_P [p1 /set1_P -> p2] ->]. rewrite H // osum0r //; exact: (Os_ordinal oc p2). move => tc; apply /funI_P; exists (J \0o t). by apply:setXp_i; fprops; apply/set1_P. aw; rewrite H // osum0r //; exact:(Os_ordinal oc tc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)