proposition: Lemma prod_gt0_inv (R : realFieldType) n (F : _ -> R) (HF: forall a, (0 <= F a)) : (0 < \prod_(i < n.+1) F i -> forall i, 0 < F i).
proof: Proof. move=> h i. rewrite lt_neqAle HF andbT; apply/eqP => /esym F0. move: h; rewrite ltNge => /negP; apply. rewrite le_eqVlt; apply/orP; left. rewrite prodf_seq_eq0/=. apply/hasP; exists i; last exact/eqP. by rewrite mem_index_enum. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext