The Coq mailing list

[t x <txrev319 AT gmail.com>]

Please consider the following code snipplet:

Goal forall x, (0 < Pos.to_nat x)% nat.
(* 1 *) auto with *.
(* 2 *) intros.
(* 3 *) auto with *.
(* 4 *) SearchAbout((0 < Pos.to_nat _)%nat).
(* 5 *) apply Pos2Nat.is_pos.

Neither line 1 nor line 3 solves the goal, is weird given that Line 4 finds the lemma used in Line 5.

Questions:

(1) Why does "auto with *" not solve this given (a) there is such a lemma and (b) "*" supposedly mean all Hints

(2) Where by "fix", I mean "write a tactic where if [apply _existing lemma_] can solve it, then solve it"

Thanks!