proposition: Lemma comparable_bigr x x0 op I (P : pred I) F (s : seq I) : {in >=<%O x &, forall y z, x >=< op y z} -> x >=< x0 -> {in P, forall i, x >=< F i} -> x >=< \big[op/x0]_(i <- s | P i) F i.
proof: Proof. by move=> *; elim/big_ind : _. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat choice seq) mathcomp(path fintype tuple bigop finset div prime finfun) mathcomp(finset)