task6.v

Require Import Arith.

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

task7.v

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

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

Goal forall P : nat -> Prop, (forall n m, P n -> P m) -> (exists p, P p) -> forall q, P q.
Proof.
  intros.
  destruct H0.
  apply (H x q).
  apply H0.
Qed.

task8.v

Require Import Arith.

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

task9.v

Require Import Arith.

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

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