proposition: Lemma seq_0 (start len : nat) : seq start len = map (fun x => start + x) (seq 0 len).
proof: Proof. revert start; induction len; simpl; intros. { reflexivity. } { rewrite IHlen; simpl. rewrite seq_S. rewrite map_map. apply f_equal2. { omega. } { apply map_ext; intro; omega. } } Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.ZArith.ZArith Coq.Lists.List Coq.Lists.SetoidList Coq.Bool.Bool Fiat.Common Fiat.Common.List.Operations Fiat.Common.Equality Fiat.Common.List.FlattenList Fiat.Common.LogicFacts