proposition: Lemma int_index_prove : forall (n i : int), 0 <= i -> i < n -> index n i.
proof: Proof. Proof using. intros. rewrite~ int_index_eq. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibOperation LibInt LibMonoid)