proposition: Lemma behead_rcons (xs : seq A) x : 0 < size xs -> behead (rcons xs x) = rcons (behead xs) x.
proof: Proof. by case: xs. Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat seq eqtype path fintype finfun tuple interval perm fingroup) pcm(options prelude ordtype seqext slice)