1
我試圖做一個證明在勒柯克，我想用已經definded和我證明了一個引理的推論。是否有可能爲下面的代碼？使用已經證明了LEMA /定理/在COQ
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.
在上述我想使用的事實，即A/\ B是相同B/\ A爲了證明〜（A/\ B）是相同的〜（B/\一個）。是否可以使用我的證明引理？