proposition: Lemma sier_inf_sum_prop sigma: sier_inf_sum sigma = order_type_of (order_sum Nat_order (Lg Nat (sier_inf_sum_aux sigma))).
proof: Proof. move: Nat_order_wor => [[or1 _] sr1]. rewrite /sier_inf_sum. set f := Lg Nat _. have -> : f = Lg (substrate Nat_order) (fun i => order_type_of (Vg (Lg Nat (sier_inf_sum_aux sigma)) i)). rewrite sr1; apply: Lg_exten => n nn. rewrite LgV// /sier_inf_sum_aux. rewrite - (Cantor_eta_prop2 eta_likeQ). by rewrite (OT_prod2_pr2 (ordinal_o_or _) BQor_or). have aux: order_fam (Lg Nat (sier_inf_sum_aux sigma)). hnf; aw => t tN; rewrite LgV//; apply: (orprod2_or _ BQor_or). apply: ordinal_o_or. by rewrite (OT_sum_invariant3 or1); aw. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)