2013-03-17から1日間の記事一覧
等比数列の和です. g `!n. sum(0,SUC n) (\n. &2 pow n) = &2 pow (SUC n) - &1`; e( Induct_on `n` ); e( RW_TAC(real_ss++REAL_ARITH_ss)[pow, SUM_1] ); e( RW_TAC(real_ss++REAL_ARITH_ss)[pow, sum] ); - g `!n. sum(0,SUC n) (\n. 2 pow n) = 2 pow (…