proposition: Lemma cardinal_indecomposable1 c a : infinite_c c -> a <o c -> ((c -o a) = c /\ cardinal (c -s a) = c).
proof: Proof. move => icx ax; move: (icx) => [cx _]. move: (ax) => [[oa ox _] _]. have oix:= (cardinal_indecomposable icx). have eq1:= (indecomp_prop1 oix ax). move: (odiff_pr (proj1 ax)); rewrite - {2} eq1; move => [ob bv]. split; first by symmetry; exact:(osum2_simpl ox ob oa bv). move /(ocle2P (proj1 icx) oa): ax; move: icx. rewrite -{1 2 4} (card_card cx) => /infinite_setP; apply:infinite_compl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)