using an already proved lema/theorem/corollary in coq

Question

I am trying to make a proof in Coq, and I would like to use a lemma already definded and proved by me. Is it possible for the following code?

Lemma conj_comm:
forall A B : Prop, A /\ B -> B /\ A.
Proof.
intros.
destruct H.
split.
exact H0.
exact H.
Qed.


Lemma not_conj_comm:
forall A B : Prop, ~(A /\ B) -> ~(B /\ A).
Proof.
intros.
intro.
unfold not in H.
apply H.
use H0.

In the above I want to use the fact that A /\B is the same as B /\ A in order to prove that ~(A /\ B) is the same as ~(B /\ A). Is it possible to use my proved lemma?

jspcal jspcal · Accepted Answer · 2012-11-25T17:02:04

you can use apply<lemma>.

there's an example here

http://blog.mikael.johanssons.org/archive/2007/08/coq-and-simple-group-theory/

see the line that says apply unit_uniq

using an already proved lema/theorem/corollary in coq

1 Answers