proposition: Lemma trajectD m n x : traject x (m + n) = traject x m ++ traject (iter m f x) n.
proof: Proof. by elim: m => //m IHm in x *; rewrite addSn !trajectS IHm -iterSr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)