proposition: Lemma constantP s : reflect (exists x, s = nseq (size s) x) (constant s).
proof: Proof. apply: (iffP idP) => [| [x ->]]; last exact: constant_nseq. case: s => [|x s] /=; first by exists x0. by move/all_pred1P=> def_s; exists x; rewrite -def_s. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)