proposition: Lemma int_index_le : forall i n m : int, index n i -> n <= m -> index m i.
proof: Proof. Proof using. introv. do 2 rewrite @int_index_eq. math. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibRelation LibOperation LibInt LibMonoid)