proposition: Lemma iter_nat_point a n : iter_nat a n n = a n.
proof: Proof. unfold iter_nat. rewrite Nat.sub_succ_l // Nat.sub_diag /=. by apply neutral_r. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements