proposition: Lemma nth_behead s n : nth d (behead s) n = nth d s n.+1.
proof: Proof. by case: s =>//; rewrite /= nth_nil. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2