proposition: Lemma seq_last start length : seq start (S length) = (seq start length) ++ [start + length].
proof: Proof. by rewrite -/(1 + length) (Nat.add_comm 1 length) seq_app. Qed.
imports: ssreflect ssrbool ssrfun PeanoNat Lia Permutation List