## Stream: Coq users

### Topic: ✔ [Newbie] How to prove a -> (b -> a)

#### Julin S (Apr 21 2021 at 03:00):

Hi. I'm just getting started with Coq and was trying to prove

``````a -> (b -> a)
``````

How can this be done?

I reached only here:

``````Theorem Hello: forall (a b : Prop), a -> (b->a).
Proof.
intros a b H.  (* I guess this isn't the way to go about it.. *)
Qed.
``````

#### Jasper Hugunin (Apr 21 2021 at 03:05):

At that point in your proof, you have an assumption called `H` saying that `a` holds, and your goal is to prove `b -> a`, that `b` implies `a`. The way to prove an implication is to introduce the antecedent as an assumption with `intros H2.` (where `H2` now becomes an assumption saying that `b` holds), leaving you with the goal to prove `a`. But `a` holds by the assumption `H`, so you can finish the proof with `exact H.` or `assumption.`.

#### Julin S (Apr 21 2021 at 03:14):

Thanks!

I did as you said with

``````Theorem Hello: forall (a b : Prop), a -> (b->a).
Proof.
intros a b H.
intros H2.
exact H.
Qed.
``````

And the proof finished.

#### Notification Bot (Jul 16 2021 at 07:36):

Ju-sh has marked this topic as resolved.

Last updated: Feb 06 2023 at 13:03 UTC