proposition: Lemma set_nth_nth p n : n < size p -> set_nth p n (nth p n) = p.
proof: Proof. move=> H. apply: (eq_from_nth (x0 := C.zero)). by rewrite seq.size_set_nth; apply/maxn_idPr. move=> i Hi. rewrite seq.size_set_nth in Hi. move/maxn_idPr: (H) (Hi) =>-> Hn. rewrite seq.nth_set_nth /=. by case E : (i == n); first by rewrite (eqP E). Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec