proposition: Lemma nsum_p11e f: nat_ord_seq f -> n_sum_rem f <> \1o.
proof: Proof. move => ax. rewrite /n_sum_rem; Ytac fs; first by fprops. move => v1. move: (nsum_p10a ax fs) =>[n nN np]. have h i: natp i -> n <=c i -> Vg f i = \0o. by move => qa qb; move: (proj2(np _ qa qb)); rewrite v1 => /olt1. have ss: sub (nsupport f) n. move => t/Zo_P [tN fnZ]; apply/(NltP nN). by case: (NleT_el nN tN) => // /(h _ tN). by move:(sub_finite_set ss (finite_set_nat nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)