proposition: Lemma ord_induction_p19 a b c: OIax3 u w0 g -> u <=o a -> \0o <o b -> \0o <o c -> f a (b *o c) = f (f a b) c.
proof: Proof. move=> ax3 ua b1 /oge1P c1. move:(ax3) => [[ax1 ag2 aw2w aw2] aw3 ag3 ag4]. pose p y := g y (f a b). pose F1 c := f a (b *o c). pose F2 c := f (f a b) c. have ufab : u <=o f a b by apply: (ord_induction_p41 fv ax1). have ob := proj32_1 b1. have pu: (forall x, \1o <=o x -> F2 (osucc x) = p (F2 x)). by move=> x [_ xp _];rewrite /F2(ord_induction_p13 fv (conj ax1 ag2) ufab xp). have pv: (forall x, \1o <=o x -> F1 (osucc x) = p (F1 x)). move => x /oge1P xp; rewrite /F1 (oprod2_succ ob (proj32_1 xp)). by rewrite ord_induction_p18 //; apply: oprod2_pos. have pa: normal_ofs1 F1 \1o. have bp:= ole0x (OS_prod2 ob OS1). move: (ord_induction_p10 fv ax1 ua) => /normal_ofs_equiv1 n1. apply: (normal_ofs_compose1 OS0 OS1 bp n1); apply: (normal_ofs_equiv2 OS1). by apply: oprod_normal. have pb: normal_ofs1 F2 \1o. apply: (normal_ofs_equiv2 OS1); apply:(ord_induction_p10 fv ax1 ufab). have pe: F1 \1o = F2 \1o. by rewrite /F1 /F2 (oprod1r ob) {2} fv ord_induction_y1 (aw3 _ ufab). exact:(normal_ofs_uniqueness1 pa pb OS1 pv pu pe c1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)