proposition: Lemma ord_induction_p14 (f:= ord_induction_defined id (fun u v:Set => osucc u)): (forall a b, ordinalp a -> ordinalp b -> f a b = a +o b) /\ (forall a b c, ordinalp a -> ordinalp b -> ordinalp c -> f (f a b) c = f a (f b c)).
proof: Proof. pose w0 (x:Set) := x; pose g u (v:Set) := osucc u. move: (erefl f) => ee. have H: forall u, \0o <=o u -> u <o osucc u. move => x [_ ox _]; exact (oltS ox). have ax1: OIax1 \0o w0 g. rewrite /w0 /g;split. - by move => x /H xp. - by move => x /H []. - by move => u v /H up. have ax2:OIax_g2 \0o g by move => u v x y _ _ /oleSSP uv _. have aux: forall a, ordinalp a -> forall b, ordinalp b -> f a (osucc b) = osucc (f a b). move => a /ole0x oa nb ob. by rewrite (ord_induction_p13 ee (conj ax1 ax2) oa ob). have f0: forall a, ordinalp a -> f a \0o = a +o \0o by move => a oa; rewrite /f (ord_induction_y0 w0 g a) osum0r. split. move => a b oa ob. have ap:= ole0x oa. move: (ord_induction_p10 ee ax1 ap) => nfa. have pa: (forall x, ordinalp x -> f a (osucc x) = osucc (f a x)). by move => x /(aux _ oa). have pb:(forall x, ordinalp x -> a +o osucc x = osucc (a +o x)). by move => x ox; rewrite osum2_succ. have pc: f a \0o = a +o \0o by apply: f0. move: (normal_ofs_uniqueness nfa (osum_normal oa) (p:=osucc) pa pb pc). by apply. move => a b c oa ob oc. have ap:= ole0x oa. have bp:= ole0x ob. have hh: ordinalp (f a b) by apply:(ord_induction_p5 ee ax1 ap ob). have qa: normal_ofs (fun c => f (f a b) c). apply: (ord_induction_p10 ee ax1 (ole0x hh)). have qb: normal_ofs (fun c => f a (f b c)). by apply:normal_ofs_compose; apply: (ord_induction_p10 ee ax1). have qc: forall x, ordinalp x -> f (f a b) (osucc x) = osucc (f (f a b) x). by move => x ox; rewrite aux. have qd:forall x, ordinalp x -> f a (f b (osucc x)) = osucc (f a (f b x)). by move => x ox; rewrite aux // aux //; apply:(ord_induction_p5 ee ax1). have qe: f (f a b) \0o = f a (f b \0o) by rewrite f0 // f0 // osum0r // osum0r. exact: (normal_ofs_uniqueness qa qb qc qd qe oc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)