proposition: Lemma behead_rev {T : Type} (s : seq T) : behead (rev s) = rev (belast s).
proof: Proof. case: s => // t s ; elim: s t => // t s IHs t0. rewrite rev_cons behead_rcons ?IHs ?size_rev -?rev_cons //= ; by apply Nat.lt_0_succ. Qed.
imports: Coq(Reals Psatz ssreflect) Coq(ssrbool) mathcomp(seq)