ex2.v

Require Import Arith.

Goal forall x y, x < y -> x + 10 < y + 10.
Proof.
  intros x y; apply plus_lt_compat_r.
Qed.

Goal forall P Q : nat -> Prop, P 0 -> (forall x, P x -> Q x) -> Q 0.
Proof.
  intros P Q H0 H; apply H, H0.
Qed.

Goal forall P : nat -> Prop, P 2 -> (exists y, P (1 + y)).
Proof.
  intros P P2; exists 1; assumption.
Qed.

Goal forall P : nat -> Prop, (forall n m, P n -> P m) -> (exists p, P p) -> forall q, P q.
Proof.
  intros P H [p Hp] q; eapply H, Hp.
Qed.

Goal forall m n : nat, (n * 10) + m = (10 * n) + m.
Proof.
  intros m n; rewrite mult_comm; reflexivity.
Qed.

Goal forall n m p q : nat, (n + m) + (p + q) = (n + p) + (m + q).
Proof.
  intros n m p q.
  rewrite plus_assoc.
  rewrite plus_assoc.
  rewrite <-(plus_assoc n).
  rewrite <-(plus_assoc n p).
  rewrite (plus_comm m p).
  reflexivity.
Qed.

Goal forall n m : nat, (n + m) * (n + m) = n * n + m * m + 2 * n * m.
Proof.
  intros n m.
  rewrite <-mult_assoc.
  simpl.
  rewrite plus_0_r.
  rewrite <-plus_assoc.
  rewrite (plus_comm (m * m)).
  rewrite <-plus_assoc.
  rewrite <-mult_plus_distr_r.
  rewrite plus_assoc.
  rewrite <-mult_plus_distr_l.
  rewrite (mult_comm n).
  rewrite <-mult_plus_distr_l.
  reflexivity.
Qed.