proposition: Lemma oprod_cardinal a b: ordinalp a -> ordinalp b -> cardinal (a *o b) = (cardinal a) *c (cardinal b).
proof: Proof. move => xo yo. have wox:= (ordinal_o_wor xo). have woy:= (ordinal_o_wor yo). have orx := (ordinal_o_or a). have ory := (ordinal_o_or b). have pa: worder (order_prod2 (ordinal_o a) (ordinal_o b)) by fprops. rewrite /oprod2 (cardinal_of_ordinal pa) (orprod2_sr orx ory). rewrite (ordinal_o_sr a) (ordinal_o_sr b) cprod2cl cprod2cr cprodC. symmetry;rewrite cprod2_pr1; apply /card_eqP. exists (product2_canon b a); split => //. - apply: product2_canon_fb. - by rewrite /product2_canon; aw. - by rewrite /product2_canon; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)