proposition: Lemma ord_induction_y1 w0 g x: ord_induction_defined w0 g x \1o = g (w0 x) x.
proof: Proof. rewrite (ord_induction_yp _ _ _ olt_01). by rewrite /ord_induction_sup funI_set1 setU_1 ord_induction_y0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)