proposition: Lemma sier_ex1_p3: c <> \0c -> n_sum_rem f = c *o omega0.
proof: Proof. move => cnz. have cp: \0o <o c by apply: ord_ne0_pos. apply: (nsum_eventually_const sier_ex1_p1 cp). exists (csucc n); first by apply: NS_succ. move => t tN /(cleSltP nN)/cltNge h0; rewrite /f LgV//; Ytac h1. by case: h0;rewrite h1; apply: cle0n. Ytac h2 => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)