Some Complaints

[EnderGZM]

1. How can I create a proposition like "P -> P" , or equation like "0=0" , "c=c"? Though I can make these with add_zero, and so on, I want a direct way.
2. How can I create a propostion "∃c, b=a+c" from a propostion "b=a+c"? There is no way to add "∃" sign in the propostions I have proved. "use c" can only remove the "∃" in goal.
3. I want create my lemma in my prove freely.

[EnderGZM]

p : a = b + c, q : (∃ (c : mynat), a = b + c) → b ≤ a r : (b ≤ a) → false ⊢ false

I don't know what I can do next except "apply r", but I think we need a way to create the goal forward