proposition: Lemma take_traject n k x : k <= n -> take k (traject x n) = traject x k.
proof: Proof. by move=> /subnKC<-; rewrite trajectD take_size_cat ?size_traject. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)