proposition: Lemma le_bigmin_ord_cond [x0] n m (P P' : pred nat) (F : nat -> T) : (m <= n)%N -> (forall i : 'I_m, P' i -> P i) -> \big[min/x0]_(i < n | P i) F i <= \big[min/x0]_(i < m | P' i) F i.
proof: Proof. exact: (le_big_ord_cond ge_refl). Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)