Prouver les formules logiques suivantes :
forall A B, A -> B -> A.
forall (P Q : nat -> Prop), (forall x, P x) \/ (forall x, Q x) -> forall x, P x \/ Q x.
forall (A B C : Prop), A /\ B -> C -> A /\ C.
forall (A B C D : Prop), A \/ B -> (A -> C) -> (B -> D) -> C \/ D.
forall (P Q : nat -> Prop), (exists x, P x /\ Q x) -> (exists x, P x) /\ (exists x, Q x).
forall A m n, ((S n = m) -> A) -> ((1 + n = m) -> A).
forall (A : Prop), A -> ~ ~ A.
forall (A : Prop), ~ ~ (A \/ ~ A).
forall x, negb (negb x) = x
forall x y, xorb x y = xorb y x
forall x y, xorb (negb x) y = negb (xorb y x)
Fixpoint ff (n:nat) := match n with 0 => true | S p => negb (ff p) end.Prouver
forall x y, ff (x + y) = negb (xorb (ff x) (ff y))