proposition: Lemma cdiff_Mle_gen a b c: cardinalp a -> cardinalp b -> cardinalp c -> c <=c (a +c b) -> (c -c b) <=c a.
proof: Proof. move => ca cb cc h. case:(cleT_el cc cb); first by move /cdiff_wrong=> ->; apply:cle0x. move => bc. case: (finite_or_infinite cc) => fc; last first. rewrite (cdiff_inf fc bc). case: (cleT_el cc ca) => // lac; case:(cltNge (csum_inf5 lac bc fc) h). case: (finite_or_infinite ca) => fa. move/NatP:fc => cN; move/NatP:fa => aN. move: h; rewrite - {1}(cdiff_pr (proj1 bc)). rewrite csumC;apply:(csum_le2r (NS_lt_nat bc cN) (NS_diff _ cN) aN). apply: (cleT(cdiff_ab_le_a b cc) (cle_fin_inf fc fa)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)