proposition: Lemma behead_rcons (T : Type) (s : seq T) (x : T) : s <> [::] -> behead (rcons s x) = rcons (behead s) x.
proof: Proof. by case: s. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp