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