proposition: Lemma comparable_bigl x x0 op I (P : pred I) F (s : seq I) : {in >=< x &, forall y z, op y z >=< x} -> x0 >=< x -> {in P, forall i, F i >=< x} -> \big[op/x0]_(i <- s | P i) F i >=< x.
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)