proposition: Lemma osum_fnz n X: natp n -> ord_below X n -> (exists2 i, i <c n & X i <> \0o) -> \0o <o osumf X n.
proof: Proof. move => nN ax [i]; move: n nN ax. apply:Nat_induction; first by move => _ /clt0. move => n nN Hr ax /(cltSleP nN)/cle_eqVlt lin inz. move: (true_below_rec nN ax) => [ax1 axb]. move: (OS_osumf (NS_succ nN) ax) => o1. move: (OS_osumf nN ax1) => o2. apply: (ord_ne0_pos o1); rewrite (osum_fS _ nN) => /(osum2_zero axb o2). move => [ha hb]. case: lin => lin; first by case: inz; rewrite lin. by move: (proj2(Hr ax1 lin inz)); rewrite hb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)