Library probsa.util.iota

From mathcomp Require Export ssreflect ssrnat ssrbool seq eqtype bigop.

We prove that [::t1; t1+1; ...; t2] is equal to [::t1; t1+1; ...; t2-1] ++ [::t2].

Lemma index_iota_recr :
  ∀ t1 t2, t1 ≤ t2 → index_iota t1 t2.+1 = index_iota t1 t2 ++ [::t2].
Proof.
  intros × LE; apply eq_from_nth with (x0 := 0).
  { rewrite /index_iota size_cat !size_iota //=.
    have EQ: ∃ δ , t2 = t1 + δ; [by ∃ (t2 - t1); rewrite subnKC | ].
    by elim: EQ ⇒ [δ ] ->; rewrite addKn subSn ?leq_addr // addKn addn1.
  }
  { move ⇒ i LT; rewrite /index_iota.
    move: LT; rewrite /index_iota !size_iota //= subSn // ltnS leq_eqVlt ⇒ /orP [/eqP EQ|LT].
    { rewrite nth_cat nth_iota; last by rewrite -EQ ltnS.
      by rewrite size_iota -EQ ltnn //= subnn //= EQ subnKC.
    }
    { rewrite nth_cat nth_iota.
      - by rewrite size_iota LT nth_iota.
      - by rewrite ltnS ltnW.
    }
  }
Qed.