# [isabelle] Proof breaks when stronger fact is used

Hi all,
I have a rather basic question:
Given the following constants and axioms:
typedecl T1
consts
F :: "T1 \<Rightarrow> real"
G :: "T1 \<Rightarrow> real"
C :: real
axioms
ax1: "\<exists>P. \<exists>s1\<in>P. \<exists>s2\<in>P. s1 \<noteq>
s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
ax1a: "\<exists>P. \<forall>s1\<in>P. \<forall>s2\<in>P. s1 \<noteq>
s2 \<and> F s1 < F s2 \<and> G s1 <= G s2"
ax2: "F p > 0"
ax3: "C > 0"
I can prove that "\<exists> func s. func s \<noteq> (\<lambda> s. (F
s, (C / F s)))" with
lemma lem1: "\<exists> func s. func s \<noteq> (\<lambda> s. (F s, (C / F s)))"
proof (intro exI)
have "\<forall> s1 s2 t. (F s1< F s2) --> (C / F s1) > (C / F s2)"
using ax3 ax2
by (simp add: divide_inverse real_less_def)
then show "(\<lambda> s. (F s, G s)) \<noteq> (\<lambda> s. (F s, (C
/ F s)))"
using ax1
apply (intro notI)
apply (simp add: expand_fun_eq real_mult_commute)
by (metis linorder_not_le)
qed
However, if I want to *not* use ax1 but use ax1a instead, the proof
breaks. Isn't ax1a stronger than ax1? If so, why can a proof using ax1
break when a stronger ax1a is used as a fact instead?
Any help will be appreciated.
Thanks
John

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*