proposition: Lemma T2_to_bourbaki_small a b c n: a <o Gamma_0 -> b <o Gamma_0 -> c <o Gamma_0 -> Spsi a b *o csucc (nat_to_B n) +o c <o Gamma_0.
proof: Proof. move => ha hb hc. move: (Gamma0_s_psi ha hb) => hd. move: Gamma0_p1 => h; rewrite -h in hc hd |- *. exact: (Spsi_indecomp_rec n OS_Gamma_0 OS0 hd hc). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)