proposition: Lemma ord_induction_p15 a b: \0o <o a -> ordinalp b -> ord_induction_defined (fun z:Set=> \0o) osum2 a b = a *o b.
proof: Proof. move => oa ob. set w0 := (fun _ : Set => \0o). have ax1: OIax1 \1o w0 osum2. rewrite /w0;split. - move => x xp /=;rewrite osum0l; [ by apply/oge1P | exact: (proj32 xp)]. - move => x [_ xp _] /=; rewrite osum0l;fprops. - move => u v [_ ou _] /oge1P vp. by move: (osum_Meqlt vp ou); rewrite osum0r. have ax2:OIax_g2 \1o osum2 by move => u v x y /= _ _; apply:osum_Mlele. set f := (ord_induction_defined w0 osum2). have ap: \1o <=o a by apply/oge1P. move: (ord_induction_p10 (erefl f) ax1 ap) => nfa. pose p := fun x => x +o a. have pa: (forall x, ordinalp x -> f a (osucc x) = p((f a x))). move => x ox; exact: (ord_induction_p13 (erefl f) (conj ax1 ax2) ap ox). have pb:(forall x, ordinalp x -> a *o osucc x = p (a *o x)). by move => x ox; rewrite (oprod2_succ (proj32 ap)). have pc: f a \0o = a *o \0o by rewrite /f (ord_induction_y0 w0 osum2 a) oprod0r. by apply: (normal_ofs_uniqueness nfa (oprod_normal oa) pa pb pc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)