proposition: Lemma cardinal_indecomposable x: infinite_c x -> indecomposable x.
proof: Proof. move => xc; move: (proj1 xc) => cx. split; first by exact:(ord_ne0_pos (proj1 cx) (infinite_nz xc)). move => u v le1 le2 /(f_equal cardinal). move: (proj31_1 le1) (proj31_1 le2) => ou ov. rewrite osum_cardinal // (card_card cx) => /esym eq2. move: le1 => /(ocle2P cx ou) lt1. move: (csum_inf2 (CS_cardinal v) xc lt1 eq2) => h. by move: le2 => /(ocle2P cx ov) [_ []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)