proposition: Lemma osum_negl_rec n e X: ordinalp e -> X \0c = oopow e -> natp n -> (forall i, i<c n -> X (csucc i) <o oopow e) -> osumf X (csucc n) = oopow e.
proof: Proof. move => oe x0. move: (OS_oopow oe) => oope. move: n; apply: Nat_induction. by move => _; rewrite succ_zero osum_f1 // x0. move => n nN Hrec /(true_below_rec nN) [qa qb]. rewrite (osum_fS _ (NS_succ nN)) (Hrec qa). by apply: ord_negl_opow. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)