for i, _ in enumerate(l, s) = for i in range(s, len(l) + s)

enumerate_eq_range.v

   Require Import Coq.Lists.List Coq.Bool.Bool Lia.

   Import Coq.Lists.List.ListNotations.
   
   Fixpoint _range (a b d : nat) :=
     match d with
       | 0 => []
       | S n => a :: _range (S a) b n
     end.
   
   Definition range a b := _range a b (b - a).
   
   (*
   Fixpoint less n m : bool :=
     match n, m with
       | 0, 0       => false
       | 0, S _     => true
       | S _, 0     => false
       | S n, S m   => less n m
     end.
  
   Fixpoint range (a b : nat) :=
     if less a b then
        match b with
          | 0 => []
          | S n => range a n ++ [n]
        end
     else [].
   *)
   
   Eval compute in range 0 0.
   Eval compute in range 0 5.
   Eval compute in range 5 0.
   Eval compute in range 5 10.
   
   Fixpoint enumerate (T : Type) (l : list T) (s : nat) :=
     match l with
       | [] => []
       | h :: t => (s, h) :: enumerate T t (S s) 
     end.
   
   Eval simpl in enumerate nat [0;1;2;3;4] 0.
   Eval simpl in enumerate nat [5;6;7;8;9] 5.
   
   Theorem enum_prop : forall (T : Type) (l : list T) (s : nat),
                       enumerate T l s = [] -> l = [].
   Proof.
      intros. induction l.
      - reflexivity.
      - pose proof nil_cons. symmetry. specialize (H0 T a l). discriminate.
   Qed.
   
   Theorem enum_map_prop : forall (T : Type) (l : list T) (s : nat),
                           map fst (enumerate T l s) = [] -> enumerate T l s = [].
   Proof.
      intros. cut (l = [] -> enumerate T l s = []). 2: {
        intros. now rewrite H0.
      }
      
      induction l.
      - reflexivity.
      - intros. apply H0. symmetry. pose proof nil_cons. specialize (H1 T a l). discriminate.
   Qed.
     
   Theorem enumerate_eq_range : forall (T : Type) (l : list T) (s : nat),
                                map fst (enumerate T l s) = range s (length l + s).
   Proof.
      induction l.
      - intro s. cbn. now replace (s - s) with 0 by lia.
      - induction s; cbn; rewrite IHl; unfold range.
        + replace (length l + 0) with (length l) by lia.
          replace (length l + 1 - 1) with (length l) by lia.
          now replace (length l + 1) with (S (length l)) by lia.
        + replace (length l + S (S s) - S (S s)) with (length l) by lia.
          replace (length l + S s - s) with (S (length l)) by lia; cbn.
          now replace (S (length l + S s)) with (length l + S (S s)) by lia.
   Qed.