proposition: Lemma ord_induction_zv c: ord_induction_g_unit c -> OIax1 -> [/\ (forall a, u <=o a -> (g (w0 a) a) = a), (forall a b, u <=o a -> ordinalp b -> f a (b +o \0o) = g (f a b) (f a \0o)), (forall a b, u <=o a -> ordinalp b -> f a (\0o +o b) = g (f a \0o) (f a b)), forall a b, u <=o a -> ordinalp b -> f a (b *o \0o) = f (f a b) \0o & forall a b, u <=o a -> ordinalp b -> f a (\0o *o b) = f (f a \0o) b].
proof: Proof. move => [oc gcc cwc h] ax1. have pa: forall a, u <=o a -> f a \0o = c. by move => a au; rewrite fv ord_induction_y0 (proj33 (h _ au)). split. - by move => a au; move: (h _ au) => [h1 h2 ->]. - move => a b ua ob. rewrite (osum0r ob) (pa _ ua). case: (ozero_dichot ob); first by move => ->;rewrite (pa _ ua). by move => bp; move: (h _ (ord_induction_p41 ax1 ua bp)) => [ -> _ _]. - move => a b ua ob. rewrite (osum0l ob) (pa _ ua). case: (ozero_dichot ob); first by move => ->;rewrite (pa _ ua). by move => bp; move: (h _ (ord_induction_p41 ax1 ua bp)) => [ _ -> _]. - move => a b ua ob; rewrite oprod0r (pa _ ua). case: (ozero_dichot ob). by move => ->; rewrite (pa _ ua) fv ord_induction_y0 - cwc. by move => bp; rewrite (pa _ (ord_induction_p41 ax1 ua bp)). - move => a b ua ob. rewrite oprod0l (pa _ ua) fv. move: b ob; apply: least_ordinal2 => y oy etc. move: (ord_induction_y0 w0 g c) => g0. case: (ozero_dichot oy); first by move => ->; rewrite g0. move => yp; rewrite (ord_induction_yp w0 g _ yp). rewrite / ord_induction_sup; set G := fun_image _ _. suff: G = singleton c by move => ->; rewrite setU_1. apply: set1_pr. by apply /funI_P;exists \0o; [ apply:olt_i |rewrite g0 - cwc gcc]. by move => z /funI_P [t /(oltP oy) /etc <- ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)