proposition: Lemma osum_cardinal a b: ordinalp a -> ordinalp b -> cardinal (a +o b) = (cardinal a) +c (cardinal b).
proof: Proof. move => ox oy; symmetry. rewrite /osum2. set w := order_sum2 _ _. have w1: worder w by rewrite /w;fprops. have pa:= (OS_ordinal w1). move: (ordinal_o_is w1) => [F [_ _ [bf sf tf] _]]. have /card_eqP: source F \Eq target F by exists F. rewrite tf (ordinal_o_sr (ordinal w)) sf {1} /w orsum2_sr; fprops. rewrite (ordinal_o_sr a)(ordinal_o_sr b) => <-. rewrite /canonical_du2 -/(csum _) csum_pr; apply: csum2_pr; aw. set f := fun a:Set => _. by move: (doubleton_fam_canon f); rewrite /f;aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)