proposition: Lemma big_tuple0 R idx (op : Monoid.law idx) (I : finType) P (F : 0.-tuple I -> R) : \big[op/idx]_(t : 0.-tuple I | P t) F t = if P [tuple] then F [tuple] else idx.
proof: Proof. rewrite big_mkcond (big_pred1 [tuple]) // => x /=; rewrite tuple0 (eqxx [tuple]). by []. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)