# [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
then show "(\<lambda> s. (F s, G s)) \<noteq> (\<lambda> s. (F s, (C
/ F s)))"
using ax1
apply (intro notI)
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.