proposition: Lemma behead_rev_take (T : Type) (s : seq T) (n : nat) : n <= size s -> behead (rev (take n s)) = rev (take n.-1 s).
proof: Proof. elim: n s =>[//|n IHn] [//|x s] H //. rewrite ltnS -/size in H. rewrite /=. case: n IHn H =>[//|n] /= IHn H; first by rewrite take0 //. rewrite [in RHS]rev_cons -IHn // rev_cons behead_rcons //. move/(f_equal size). fold (@take T); fold (@size T) in H. rewrite size_rev size_take. case: leq =>//=. by move=> top; rewrite top in H. Qed.
imports: Coq(ZArith Rfunctions NaryFunctions Lia) mathcomp.ssreflect(ssreflect ssrbool ssrfun eqtype ssrnat seq fintype bigop tuple) MathComp