proposition: Lemma csucc_inf x: infinite_c x <-> x = csucc x.
proof: Proof. split. by rewrite csuccE; move => [sa /card_eqP <- ]; rewrite card_card. move => h; rewrite h; split; first by apply: CS_succ. apply/card_eqP;rewrite - {2}h; exact: card_csucc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)