(**
 * Some lemmas about inject_nat, absolu and the relation between
 * Z and nat in general.
 *)

Require ZArith.
Require EqNat.

Require lemmas.

Lemma abs_opp: (x:Z)(absolu x)=(absolu `-x`).
Proof.
   Induction x.
   Simpl. Reflexivity.
   Simpl. Reflexivity.
   Simpl. Reflexivity.
Qed.

Lemma inj_abs_pos: (x:Z)`x>=0` -> (inject_nat (absolu x))=x.
Proof.
   Induction x.
   Reflexivity.
   Intros. Simpl.
   Induction p.
   Rewrite POS_xI.
   Rewrite <- Hrecp.
   Replace (convert (xI p)) with (S (mult (2) (convert p))).
   Rewrite inj_S.
   Rewrite inj_mult.
   Rewrite Hrecp.
   Simpl.
   Reflexivity.
   Apply Zle_ge. Apply ZERO_le_POS.
   Replace (2) with (convert (xO xH)).
   Rewrite <- times_convert.
   Simpl.
   Rewrite <- bij1.
   Rewrite bij2.
   Simpl.
   Reflexivity.
   Simpl.
   Reflexivity.
   Apply Zle_ge. Apply ZERO_le_POS.
   Rewrite POS_xO.
   Rewrite <- Hrecp.
   Replace (convert (xO p)) with (mult (2) (convert p)).
   Rewrite inj_mult.
   Rewrite Hrecp.
   Simpl.
   Reflexivity.
   Apply Zle_ge. Apply ZERO_le_POS.
   Replace (2) with (convert (xO xH)).
   Rewrite <- times_convert.
   Simpl.
   Reflexivity.
   Simpl.
   Reflexivity.
   Apply Zle_ge.
   Apply ZERO_le_POS.
   Reflexivity.
   Intros.
   Elim H.
   Simpl.
   Reflexivity.
Qed.

Lemma inj_abs_neg: (x:Z)`x<0` -> (inject_nat (absolu x))=`-x`.
Proof.
   Intros.
   Rewrite abs_opp.
   Apply inj_abs_pos.
   Apply Zle_ge.
   Apply Zsimpl_le_plus_l with x.
   Rewrite <- Zplus_n_O.
   Rewrite Zplus_inverse_r.
   Apply Zlt_le_weak.
   Assumption.
Qed.

Lemma abs_inj: (n:nat)(absolu (inject_nat n))=n.
Proof.
   Induction n.
   Simpl. Reflexivity.
   Intros m IH.
   Rewrite <- IH. Simpl.
   Rewrite bij1.
   Reflexivity.
Qed.

Lemma abs_mult: (x,y:Z)(absolu `x*y`)=(mult (absolu x) (absolu y)).
Proof.
   Induction x.
   Simpl. Intro. Reflexivity.
   Intro.
   Induction y.
   Simpl.
   Rewrite <- mult_n_O.
   Reflexivity.
   Intro.
   Simpl.
   Rewrite <- times_convert.
   Reflexivity.
   Simpl.
   Intro.
   Rewrite <- times_convert.
   Reflexivity.
   Intro.
   Induction y.
   Simpl.
   Rewrite <- mult_n_O.
   Reflexivity.
   Intro.
   Unfold absolu.
   Simpl.
   Rewrite <- times_convert.
   Reflexivity.
   Intro.
   Unfold absolu.
   Simpl.
   Rewrite <- times_convert.
   Reflexivity.
Qed.

Lemma isnat_inj_abs: (x:Z; n:nat)`x=(inject_nat n)`->n=(absolu x).
Proof.
   Intros.
   Rewrite H.
   Rewrite abs_inj.
   Reflexivity.
Qed.

Lemma isnat_abs_inj: (x:Z)(n:nat)`0<=x`->n=(absolu x)->`x = (inject_nat n)`.
Proof.
   Intros.
   Rewrite H0.
   Rewrite inj_abs_pos.
   Reflexivity.
   Apply Zle_ge.
   Assumption.
Qed.

Lemma isnat_plus: (x,y:Z)`0 <= x` -> `0 <= y` -> `0 <= x+y`.
Proof.
   Induction x. Simpl. Intros. Assumption.
   Intro. Induction y. Simpl. Intros. Assumption.
   Simpl. Intros. Unfold Zle. Simpl. Discriminate.
   Intros. Unfold Zle in H0. Elim H0. Simpl. Reflexivity.
   Intros. Unfold Zle in H. Elim H. Simpl. Reflexivity.
Qed.

Lemma isnat_mult: (x,y:Z)`0 <= x` -> `0 <= y` -> `0 <= x*y`.
Proof.
   Induction x.
   Simpl. Intros. Unfold Zle. Simpl. Discriminate.
   Intro. Induction y. Simpl. Intros. Unfold Zle. Simpl. Discriminate.
   Simpl. Intros. Unfold Zle. Simpl. Discriminate.
   Intros. Unfold Zle in H0. Elim H0. Simpl. Reflexivity.
   Intros. Unfold Zle in H. Elim H. Simpl. Reflexivity.
Qed.


Lemma lezle: (x,y:Z)`0 <= x`->`0 <= y`->`x <= y`->(le (absolu x) (absolu y)).
Proof.
   Intros.
   Elim (le_or_lt (absolu x) (absolu y)).
   Intros. Assumption.
   Intros. Elim (Zlt_not_le y x).
   Rewrite <- (inj_abs_pos x).
   Rewrite <- (inj_abs_pos y).
   Apply inj_lt. Assumption.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Assumption.
   Assumption.
Qed.

Lemma gtzgt: (x,y:Z)`0 <= x`->`0 <= y`->`x > y`->(gt (absolu x) (absolu y)).
Proof.
   Intros.
   Elim (le_or_lt (absolu x) (absolu y)).
   Intros.
   Elim (Zle_not_lt x y).
   Rewrite <- (inj_abs_pos x).
   Rewrite <- (inj_abs_pos y).
   Apply inj_le. Assumption.
   Apply Zle_ge. Assumption.
   Apply Zle_ge. Assumption.
   Apply Zgt_lt. Assumption.
   Unfold gt. Intro. Assumption.
Qed.

Lemma ltzlt: (x,y:Z)`0<=x`->`0<=y`->`x<y`->(lt (absolu x) (absolu y)).
Proof.
   Intros.
   Change (gt (absolu y) (absolu x)).
   Apply gtzgt. Assumption. Assumption.
   Apply Zlt_gt. Assumption.
Qed.

Lemma abs_plus_pos:
   (x,y:Z)`0 <= x`->`0 <= y`->(absolu `x+y`)=(plus (absolu x) (absolu y)).
Proof.
   Induction x.
   Simpl.
   Intros.
   Reflexivity.
   Intro.
   Induction y.
   Simpl.
   Rewrite <- plus_n_O.
   Intros.
   Reflexivity.
   Simpl.
   Intros.
   Apply convert_add.
   Intros.
   Unfold Zle in H0.
   Simpl in H0.
   Elim H0.
   Reflexivity.
   Intros.
   Unfold Zle in H.
   Simpl in H.
   Elim H.
   Reflexivity.
Qed.

Lemma abs_minus_pos:
   (x,y:Z)`0<=x`->`0<=y`->`x>=y`->(absolu `x-y`)=(minus (absolu x) (absolu y)).
Proof.
   Intros.
   Elim (inject_nat_complete x).
   Intros nx Hx.
   Elim (inject_nat_complete y).
   Intros ny Hy.
   Elim (inject_nat_complete `x-y`).
   Intros d Hd.
   Rewrite Hx.
   Rewrite Hy.
   Rewrite <- inj_minus1.
   Rewrite abs_inj.
   Rewrite abs_inj.
   Rewrite abs_inj.
   Reflexivity.
   Rewrite (isnat_inj_abs x nx).
   Rewrite (isnat_inj_abs y ny).
   Apply lezle.
   Assumption.
   Assumption.
   Apply Zge_le.
   Assumption.
   Assumption.
   Assumption.
   Unfold Zminus.
   Apply Zle_left.
   Apply Zge_le.
   Assumption.
   Assumption.
   Assumption.
Qed.

Lemma abs_pred_pos: (x:Z)`0<x`->(pred (absolu x))=(absolu `x-1`).
Proof.
   Intros.
   Rewrite abs_minus_pos.
   Replace (absolu `1`) with (1).
   Rewrite predminus1.
   Reflexivity.
   Reflexivity.
   Apply Zlt_le_weak.
   Assumption.
   Unfold Zle.
   Simpl.
   Discriminate.
   Apply Zle_ge.
   Change `(Zs 0) <= x` .
   Apply Zlt_le_S.
   Assumption.
Qed.

Lemma abs_neq_lt: (x:Z)`x<>0`->(lt O (absolu x)).
Proof.
   Induction x.
   Intro. Elim H. Reflexivity.
   Intros. Change (lt (absolu `0`) (absolu (POS p))). Apply ltzlt.
   Unfold Zle. Simpl. Discriminate.
   Unfold Zle. Simpl. Discriminate.
   Unfold Zlt. Simpl. Reflexivity.
   Intros. Change (lt (absolu `0`) (absolu (POS p))). Apply ltzlt.
   Unfold Zle. Simpl. Discriminate.
   Unfold Zle. Simpl. Discriminate.
   Unfold Zlt. Simpl. Reflexivity.
Qed.