の絶対値の積分において，絶対値記号を外に出すには定符号を言えば良いわけです．もし変数変換が使えるならに帰着する道もありそうですが，それらしいthmは見当たりませんので，の偶奇により場合を分けて行きます． g `!m y. (&2 * &m) * pi <= y /\ y <= (&…

次は積分の平均値定理ですが，第２はありますが，簡単な第１が見当たらないので，CONT_ATTAINS_ALLとIVTなどから証明しました． let thm12 = MESON[thm05; REAL_LE_TRANS] `(!x. &0 <= x /\ x <= &1 ==> f contl x) ==> !n. 1 <= n ==> !k. 1 <= k /\ k <= n…