proposition: Lemma eq_big_widen {P : pred T} {F : T -> S}: (forall x, sT x -> rT x) -> (forall x, ~~ sT x -> F x = idx) -> \big[op/idx]_(x : I | P (val x)) (F (val x)) = \big[op/idx]_(x : J | P (val x)) (F (val x)).
proof: Proof. move=> h1 h2; rewrite big_sub_widen //; apply/esym. rewrite (bigID (sT \o val)) [X in op _ X]big1 ?Monoid.simpm //. by move=> j /andP [_ /h2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset order) mathcomp(ssralg)