16 lines
265 B
Coq
Executable file
16 lines
265 B
Coq
Executable file
Require Import Naturelle.
|
|
Section Session1_2019_Logique_Exercice_2.
|
|
|
|
Variable A B : Prop.
|
|
|
|
Theorem Exercice_2_Naturelle : (~A) \/ B -> (~A) \/ (A /\ B).
|
|
|
|
Theorem Exercice_2_Coq : (~A) \/ B -> (~A) \/ (A /\ B).
|
|
intros.
|
|
|
|
|
|
Qed.
|
|
|
|
End Session1_2019_Logique_Exercice_2.
|
|
|