proposition: Lemma int_index_succ : forall n i, n >= 0 -> index (n + 1) i = (index n i \/ i = n).
proof: Proof. Proof using. introv P. do 2 rewrite int_index_eq. extens. iff H. apply or_classic_l. math. destruct H; math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibOperation LibInt LibMonoid)