proposition: Lemma OS_sum r g: worder_on r (domain g) -> ordinal_fam g -> ordinalp (osum r g).
proof: Proof. move=> [or sr] alo ; apply: OS_ordinal. apply: orsum_wor; [ saw | hnf; aw => i idg; rewrite LgV //; fprops]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)