proposition: Lemma osum_cardinal_gen r X: worder_on r (domain X) -> ordinal_fam X -> cardinal (osum r X) = csumb (domain X) (fun z => cardinal (Vg X z)).
proof: Proof. move => sa sb. set Y := (Lg (domain X) (fun z => ordinal_o (Vg X z))). have hb: worder_fam Y. rewrite /Y /worder_fam /allf Lgd. move => i idx;rewrite LgV //; apply: ordinal_o_wor; apply:(sb _ idx). have hc:worder (order_sum r Y) by apply:orsum_wor; rewrite /Y; aw. have hd:orsum_ax r Y. move: sa => [[or _]dr]. have sr:substrate r = domain Y by rewrite /Y; aw. by split => // i /hb []. rewrite /osum -/Y (cardinal_of_ordinal hc) (orsum_sr hd). rewrite /sum_of_substrates -/(csum _) csum_pr /fam_of_substrates /Y !Lgd. by apply: csumb_exten => i idx; rewrite !LgV //ordinal_o_sr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)