Re: [isabelle] Natural property
a * 1 < b * (a + 1)
I would demonstrate the thesis but I don't know how to do that.
You just need to use the Ex-Introduction rule, i.e. append
apply(rule_tac x="1" in exI) apply (rule_tac x="a+1" in exI)
to your proof.
Nicer still, and more in the Isar spirit:
- Replace "proof -" by "proof (intro exI)". This applies exI in
leaving you a schematic goal.
- Replace the last "have" by "show", since this is already an instance
of the goal.
- add "qed" in the end :-)
If you had only one existential quantifier instead of two, you could
even drop the "(intro exI)", but in your case, this would only
eliminate one of the quantifications... The "intro" method applies the
supplied introduction rules repeatedly.
This archive was generated by a fusion of
Pipermail (Mailman edition) and