proposition: Lemma rcons_nseq n (x : A) : rcons (nseq n x) x = nseq n.+1 x.
proof: Proof. by elim: n=>//=n ->. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)