Require Export Arith.
Require Export Plus.
Require Export Mult.
Require Import AC.
Require Import HS.

Open Scope nat_scope.

Notation "p .1" := (fst p) (at level 20) : nat_scope.
Notation "p .2" := (snd p) (at level 20) : nat_scope.


Notation "0" := 0 (at level 11) : nat_scope.
Notation "1" := 1 (at level 11) : nat_scope.


Notation "t1 = t2" := (t1 = t2) (at level 70).

Section NAT.



Lemma plus_simpl_l : ∀ n m p : nat, m = p → n + m = n + p.
intros.
elim H; auto.
Qed.

Lemma mult_simpl_l : ∀ n m p : nat, m = p → n × m = n × p.
intros.
elim H; auto.
Qed.

Lemma mult_permute : ∀ n m p : nat, n × (m × p) = m × (n × p).
intros.
elim (mult_comm p n).
elim (mult_assoc_reverse m p n).
elim (mult_comm n).
auto.
Qed.

Lemma mult_plus_distr_l : ∀ n m p : nat, p × (n + m) = p × n + p × m.
intros.
rewrite (mult_comm p).
rewrite (mult_plus_distr_r n m p).
repeat elim (mult_comm p); auto.
Qed.

End NAT.

Ltac CNa := intros; ac_of eq plus plus_comm plus_permute; auto.

Ltac ANa := intros; repeat elim plus_assoc.

Ltac ACNa :=
  intros; repeat elim plus_assoc; ac_of eq plus plus_comm plus_permute; auto.

Ltac HSNa := intros; hs_of eq plus plus_comm plus_permute plus_simpl_l.

Ltac CNm := intros; ac_of eq mult mult_comm mult_permute; auto.

Ltac ANm := intros; repeat elim mult_assoc.

Ltac ACNm :=
  intros; repeat elim mult_assoc; ac_of eq mult mult_comm mult_permute; auto.

Ltac HSNm := intros; hs_of eq mult mult_comm mult_permute mult_simpl_l.