前回の実行結果です． # g`!a b c d. &0<a /\ &0<b ==> ( a*c<b*d <=> c/b<d/a )`;; val it : goalstack = 1 subgoal (1 total) `!a b c d. &0 < a /\ &0 < b ==> (a * c < b * d <=> c / b < d / a)` # e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`&0 < a`] 1 [`&0 < b`] `a * c < b * d <=> c / b < d / a…</d/a></b*d></a>

今回は http://as305.dyndns.org/aps/problem/view/50 すなわち [tex:\forall n:num.\, 3\le n \to (n+1)^n g`!a b c d. &0 < a /\ &0 < b ==> ( a*c<b*d <=> c/b<d/a )`;; e(REPEAT STRIP_TAC);; e(ONCE_REWRITE_TAC[ARITH_RULE`x<y<=>x-y< &0`; ]);; e(ASM_SIMP_TAC[RAT_LEMMA3]);; e(ASM_SIMP_TAC[REAL_SOSFIELD`&0<x ==>(a*b* …</x></d/a></b*d>