proposition: Lemma in_val_rm_val i j bs : in_val i (rm_val j bs) = (i != j) && in_val i bs.
proof: Proof. elim: bs i j => [[|i] [|j]|b bs IH [|i] [|j]] //=; first by rewrite andbF. - by case: bs IH. - by case: b => //; case: rm_val. - by case: bs IH => [|b1 bs] IH //=; rewrite in_val_nil. case: rm_val (IH i j) => [|b2 bs2] /=. by case: b => /=; rewrite in_val_nil; case: in_val; rewrite (andbT, andbF). by case: b. Qed.
imports: mathcomp(all_ssreflect) mathcomp(zify)