proposition: Lemma cdiff_inf a b: infinite_c a -> b <c a -> a -c b = a.
proof: Proof. move => ica lba. move: (cdiff_pr (proj1 lba)) => /esym h1. by rewrite - (csum_inf2 (CS_diff _ _) ica lba h1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)