Sample proofs from books.

ProofsOnBooks.v

(* 新妻弘，「演習　群・環・体　入門」，共立出版株式会社 より *)
Require Import ZArith.
Open Scope Z_scope.

Theorem thm_1_1 : forall a b c : Z , a + b = a + c -> b = c.
Proof.
  intros a b c H.
  apply Z.add_cancel_l with (p := a).
  assumption.
Qed.

Theorem thm_1_2_1 : forall a : Z , 0 * a = 0.
Proof.
  intros a.
  auto.
Qed.

Theorem thm1_2_2 : forall a : Z , a * 0 = 0.
Proof.
  intros.
  rewrite Z.mul_0_r.
  reflexivity.
Qed.

Theorem thm1_2_3 : forall a : Z , a * 0 = 0 * a.
Proof.
  simpl.
  intro a.
  apply thm1_2_2.
Qed.

Theorem thm1_3_1 : forall a : Z , - ( - a ) = a.
Proof.
  intros.
   rewrite <- Z.opp_involutive.
   reflexivity.
Qed.


(* 山田俊行，「はじめての数理論理学」，森北出版 より *)
Theorem thm_p_61 :
forall P Q R S : Prop, (P /\ Q) /\ (P -> R /\ S) -> S.
Proof.
  intros.
  destruct H.
  destruct H.
  destruct H0 as [H2].
  exact H.
  exact H0.
Qed.