proposition: Lemma OS_osumf n f: natp n -> ord_below f n -> ordinalp (osumf f n).
proof: Proof. move: n;apply: Nat_induction. by move => _; rewrite osum_f0; fprops. move => n nN Hrec /(true_below_rec nN) [/Hrec h1 h2]. rewrite (osum_fS _ nN); apply: (OS_sum2 h2 h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)