proposition: Lemma iter_nat_ext_loc (a b : nat -> T) (n m : nat) : (forall k, (n <= k <= m)%nat -> a k = b k) -> iter_nat a n m = iter_nat b n m.
proof: Proof. intros Heq. apply iter_ext. intros k Hk. apply Heq. by apply In_iota. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements