proposition: Lemma drop_correct sv st n : RelP sv st -> RelP (drop n sv) (drop n st).
proof: Proof. by move=> Hs k; rewrite !nth_drop; apply: Hs. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2