proposition: Lemma traject_next x0 s : uniq s -> traject (next s) (head x0 s) (size s) = s.
proof: Proof. move=> uniq_s; apply: (@eq_from_nth _ x0); rewrite size_traject // => i i_lt_s. rewrite (set_nth_default (head x0 s)) ?size_traject //. by rewrite nth_traject // iter_next_nth. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect)