proposition: Lemma big_pred1_inj (A C : finType) h i (k : A -> C) : injective k -> \big[op/idx]_(a | k a == k i) h a = h i.
proof: Proof. by move=> ?; rewrite (big_pred1 i) // => ?; rewrite eqtype.inj_eq. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum matrix) logb ssr_ext ssralg_ext