proposition: Lemma w_eq0 i : (w i == 0) = (i == ord0).
proof: Proof. apply/idP/idP => [|/eqP ->]; last by rewrite wE0. apply: contraTT => i0. rewrite {1}/w sum_nat_eq0 negb_forall. have @zero : 'I_i by exists 0; rewrite lt0n. by apply/existsP; exists zero => /=; rewrite expn_eq0 card_ord. Qed.
imports: mathcomp(all_ssreflect path ssralg ssrnum) ssr_ext