proposition: Lemma all_sums_p3 f: nat_ord_seq f -> ~ (allf f (fun z => z = \0o)) -> \0o <o n_sum f.
proof: Proof. move => ax;case :(all_exists_dichot1(fun z => Vg f z = \0o) (domain f)) => //. move => [n nN bnz] _. apply: ord_ne0_pos; first by apply: OS_nsuma. rewrite (proj32 ax) in nN; rewrite (nsum_p2 ax nN). have rd: ordinalp (Vg f n) by apply: (proj33 ax); rewrite (proj32 ax). move/(osum2_zero (OS_nsumb ax nN)(OS_nsumc ax nN)); move => /proj2. rewrite (nsum_p4 ax nN). by move/(osum2_zero rd (OS_nsumc ax (NS_succ nN))) => /proj1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)