case tail b bs MEM IH => {
  intros H;
  apply IH;
  simp at H;
  rewrite [<- Nat.nonzero_iff_gt_zero] at *;
  simp[H];
}
xs : List ℕ
x b : ℕ
bs : List ℕ
MEM : List.Mem x bs
IH : shapeProd bs > 0 → x > 0
⊢ shapeProd (b :: bs) > 0 → x > 0
no goals