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