The Coq mailing list

["Bauer, Robert" <rbauer AT rational.com>]

Hi,

I want to complete a simple proof without using "auto" - here's the relevant
part:

a: Prop
b: Prop
H: a /\ b
H0 : a
H1 : b
============
a \/ b

I know that a -> a \/ b, but can't seem to figure out what command to give
for the next step in the proof.

Along the same lines, suppose I had

H0: a
H1: a->b
========
b

In hol, I would do something like modus ponens on the assumptions, and
rewrite - I can't figure out how to do the modus ponens on the
assumption to get H2: b - so that I could use Exact.

Thanks.