proposition: Lemma Spsi_indecomp_rec u v a b n (x := Spsi u v): ordinalp u -> ordinalp v -> a <o x -> b <o x -> a *o csucc (nat_to_B n) +o b <o x.
proof: Proof. move => ou ov ax bx. move:(Spsi_indecomposable ou ov); rewrite -/x => Ha. have Hb: forall a' b', a' <o x -> b' <o x -> a' +o b' <o x. move => a' b' a'x b'x;apply:(indecomp_prop2 a'x b'x Ha). apply: (Hb _ _ _ bx). move:(proj31_1 ax) => oa. have Hc: forall m, natp m -> a *o m <o x. apply: Nat_induction. rewrite oprod0r; exact: (ole_ltT (ole0x oa) ax). move => m mN Hrec. by rewrite (succ_of_nat mN) (oprod2_succ oa (OS_nat mN)); apply: Hb. apply: Hc; apply: (NS_succ (nat_to_B_Nat n)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)