proposition: Lemma iter_nat_Chasles a n m k : (n <= S m)%nat -> (m <= k)%nat -> iter_nat a n k = op (iter_nat a n m) (iter_nat a (S m) k).
proof: Proof. intros Hnm Hmk. rewrite -iter_cat //. pattern (S m) at 2 ; replace (S m) with (ssrnat.addn n (S m - n)). rewrite -?(iota_add n (S m - n)) -?(iotaD n (S m - n)). apply (f_equal (fun k => iter _ _ (iota n k) _)). change ssrnat.addn with Peano.plus. lia. change ssrnat.addn with Peano.plus. lia. Qed.
imports: Coq(Reals Lia List ssreflect ssrbool) mathcomp(seq eqtype) Rcomplements