proposition: Lemma osum_negl_recd X n: natp n -> opos_below X (csucc n) -> (forall i, i<c n -> odegree (X (csucc i)) <o odegree (X \0c)) -> osumf X (csucc n) = X \0c.
proof: Proof. move => nN ha hb. move:(ha _ (succ_positive n)) => pa; move :(proj32_1 pa) => pb. move: n nN ha hb; apply: Nat_induction; first by rewrite succ_zero osum_f1. move => n nN Hrec /(true_below_rec (NS_succ nN)) [qa qb]. move /(true_below_rec nN) => [qc qd]. by rewrite (osum_fS _ (NS_succ nN)) (Hrec qa qc); apply: ord_negl_p7. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)