proposition: Lemma orsum_invariant3 r g: worder_on r (domain g) -> worder_fam g -> ordinal (order_sum r g) = osum r (Lg (substrate r) (fun i => ordinal (Vg g i))).
proof: Proof. move => [wor sr] alo. have or: order r by fprops. apply: ordinal_o_isu1. - by apply: orsum_wor. - apply: orsum_wor; [ by aw | hnf; aw => i isr; rewrite !LgV//; aw; trivial]. by rewrite sr in isr; apply: (ordinal_o_wor (OS_ordinal (alo _ isr))). - apply: orsum_invariant2 => //; aw; trivial. rewrite sr => i isr; rewrite !LgV //; last by aw. apply: (ordinal_o_is (alo _ isr)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)