proposition: Lemma all_pred1P x s : reflect (s = nseq (size s) x) (all (pred1 x) s).
proof: Proof. elim: s => [|y s IHs] /=; first by left. case: eqP => [->{y} | ne_xy]; last by right=> [] [? _]; case ne_xy. by apply: (iffP IHs) => [<- //| []]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)