proposition: Lemma infinite_card_limit1 x: infinite_c x -> x = opred x.
proof: Proof. move => icx. move: icx => [ /cardinalP [ox cyp] iz]. case: (osuccVpred ox) => // - [y oy yz]. have /cyp [] : inc y x by rewrite yz; fprops. apply: EqS;rewrite yz; apply/ (infinite_sP oy); ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)