proposition: Lemma sier_ex1_p2: (c = \0c) <-> finite_set (nsupport f).
proof: Proof. split => hyp. have ra: sub (nsupport f) (csucc n). move => t /Zo_P [iN]; rewrite /f LgV//; Ytac ha. by rewrite ha => _; apply/(NleP nN); apply: cle0n. by Ytac hb => // _; apply/(NleP nN). exact: (sub_finite_set ra (finite_set_nat (NS_succ nN))). have sn: sub (nsupport f) Nat by apply: Zo_S. move: (finite_subset_Nat_bis sn hyp) => [m] mN mp; ex_middle bad. move: (Nmax_p1 (NS_succ nN) mN). set k := cmax _ _; move => [kN /(cleSltP nN) /cleNgt qb /cleNgt qc]. case: (inc_or_not k (nsupport f)); first by move/mp. case; apply:(Zo_i kN); rewrite /f LgV//; Ytac ha; last by Ytac hb. by case: qb; rewrite ha; apply: cle0n. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)