proposition: Lemma addb_nseq b : forall r v, size v = r -> [seq x.1 (+) x.2 | x <- zip (nseq r b) v] = map (pred1 (negb b)) v.
proof: Proof. elim=> [ [] // | r IH [|h t] //= [] r_t]. rewrite {}IH //; move: b h; by case; case. Qed.
imports: mathcomp(all_ssreflect fingroup perm)