proposition: Lemma sier_ex1_p4: c <> \0c -> sub (n_sum_small_idx f) (csucc n).
proof: Proof. move => cnz. have cp: \0o <o c by apply: ord_ne0_pos. move /sier_ex1_p2: (cnz) => fs. move: (sier_ex1_p3 cnz). rewrite /n_sum_rem /n_sum_small_idx; Ytac0; Ytac0 => rv. move => i /Zo_P [iN]; rewrite rv /f LgV// => fv; apply/(NleP nN). move: fv; Ytac ha; first by rewrite ha => _ ; apply: cle0n. Ytac hb => // le. case: (oltNge (proj32 (indecomp_prod2 cp)) le). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)