proposition: Lemma nsum_p5 f n: nat_ord_seq f -> natp n -> n_sum_from_n f n = \0o -> (forall m, natp m -> n <=c m -> Vg f m = \0o) /\ (forall m, natp m -> n <=c m -> n_sum_from_n f m = \0o).
proof: Proof. move => ax nN rs. have aux m: natp m -> n_sum_from_n f m = \0o -> Vg f m = \0o/\ n_sum_from_n f (csucc m) = \0o. move => mN; rewrite (nsum_p4 ax mN). have rd: ordinalp (Vg f m) by apply: (proj33 ax); rewrite (proj32 ax). by move/(osum2_zero rd (OS_nsumc ax (NS_succ mN))). have ra : (forall m : Set, natp m -> n <=c m -> n_sum_from_n f m = \0o). apply: Nat_induction; first by move/cle0 => <-. move => m mN Hr; case/(cle_eqVlt); first by move <-. by move/(cltSleP mN) => /Hr /(aux _ mN) /proj2. split => //. move => m mN ll; exact: (proj1 (aux _ mN (ra _ mN ll))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)