proposition: Lemma nsum_p11a f: nat_ord_seq f -> (forall i, natp i -> Vg f i <=o (Vg f (csucc i))) -> n_sum_small_idx f = emptyset.
proof: Proof. move => ha hb. have mn i j: natp j -> i <=c j -> Vg f i <=o Vg f j. move: j; apply: Nat_induction. move/cle0 ->; exact (oleR (proj31 (hb _ NS0))). move => n nN Hrec; move: (hb _ nN) => lea. case /(cle_eqVlt); first by move ->; exact: (oleR (proj32 lea)). move/(cltSleP nN) => /Hrec leb; exact (oleT leb lea). case: (all_exists_dichot1 (fun i => Vg f i = \0o) Nat). move => H. have se: nsupport f = emptyset. by apply/set0_P => i /Zo_P [ iN]; case; apply: H. by rewrite /n_sum_small_idx se (Y_true emptyset_finite). move => [j jN jv]. move:(ha) =>[_ hc hd]. have jp: \0o <o Vg f j by apply: (ord_ne0_pos _ jv); apply: hd; ue. case: (p_or_not_p (finite_set (nsupport f))) => fs. have ss: sub (nsupport f) Nat by apply: Zo_S. move: (finite_subset_Nat_bis ss fs) =>[n nN] np. pose i := cmax j n. move: (Nmax_p1 jN nN) =>[qa qb qc]. move: (nesym (proj2 (olt_leT jp (mn _ _ qa qb)))) => qd. have:inc (cmax j n) (nsupport f) by apply: Zo_i. by move/np => /cltNge. rewrite /n_sum_small_idx; Ytac0. move: (nsum_p10a ha fs) =>[n nN np]. apply/set0_P => i /Zo_P [iN]; apply: oltNge. case: (NleT_el nN iN) => hi; first exact: (proj2 (np i iN hi)). move: (proj2 (np n nN (cleR (CS_nat nN)))) => sa. exact: (ole_ltT (mn _ _ nN (proj1 hi)) sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)