proposition: Lemma iter_nat_S a n m : iter_nat (fun n => a (S n)) n m = iter_nat a (S n) (S m).
proof: Proof. rewrite /iter_nat iter_comp. apply (f_equal (fun l => iter _ _ l _)). rewrite MyNat.sub_succ. elim: (S m - n)%nat {1 3}(n) => {n m} [ | n IH] m //=. by rewrite IH. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements