proposition: Lemma OS_prod r g: worder_on r (domain g) -> ordinal_fam g -> finite_set (substrate r) -> ordinalp (oprod r g).
proof: Proof. move=> osr alo fs; apply: OS_ordinal. apply: orprod_wor => //; [ by aw| hnf; aw=> i idg; rewrite LgV//; fprops ]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)