proposition: Lemma set_nth_correct sv st bv bt n : RelP sv st -> Rel bv bt -> RelP (set_nth dv sv n bv) (set_nth dt st n bt).
proof: Proof. by move=> Hs Hb k; rewrite !nth_set_nth /=; case: ifP. Qed.
imports: Coq(Rdefinitions Raxioms RIneq Rbasic_fun) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq bigop) MathComp1or2