Example (22.5)

　今回は，奇数分の偶数と表せる有理数が加法について閉じていることの証明です．

let lemma01 = MESON[ODD_EXISTS; LT_0; REAL_LT]`!x. ODD x ==> &0 < &x`;;
g`!a b c d. EVEN a /\ EVEN c /\ ODD b /\ ODD d ==> ?x y. &a / &b + &c / &d = &x / &y /\ EVEN x /\ ODD y`;;
e(REPEAT STRIP_TAC);;
e(ASM_SIMP_TAC[MP (REAL_FIELD`&0 < &b /\ &0 < &d ==> &a / &b + &c / &d = (&a * &d + &c * &b) / (&b * &d)`) (UNDISCH(UNDISCH(MESON[lemma01]`ODD b ==> ODD d ==> &0 < &b /\ &0 < &d`)))]);;
e(MP_TAC (MESON[EVEN_MULT; EVEN_ADD; ODD_MULT]`EVEN a /\ EVEN c /\ ODD b /\ ODD d ==> EVEN (a * d + c * b) /\ ODD (b * d)`) THEN ASM_SIMP_TAC[REAL_MUL; REAL_ADD] THEN REPEAT STRIP_TAC);;
e(ASM_MESON_TAC[]);;
let thm6 = top_thm();;