Require ZArith.
Require EqNat.

(* Some technical lemmas (mostly about le, lt, and mult)... *)

Lemma predminus1: (n:nat)(pred n)=(minus n (1)).
Proof.
   Intro n. Case n.
   Simpl. Reflexivity.
   Simpl. Intro m. Rewrite <- minus_n_O. Reflexivity.
Qed.

Lemma le_mult_l: (p,q:nat)(le p q)->(r:nat)(le (mult r p) (mult r q)).
Proof.
   Intros p q H.
   Induction r.
   Simpl.
   Apply le_n.
   Intros r1 IHr1.
   Simpl.
   Apply le_plus_plus.
   Assumption.
   Assumption.
Qed.


Lemma lt_plus_plus: (n,m,p,q:nat)(lt n m)->(lt p q)->(lt (plus n p) (plus m q)).
Proof.
   Intros n m p q H H0.
   Elim H; Simpl; Auto with arith.
Qed.


Lemma lt_mult_l: (p,q:nat)(lt p q)->(r:nat)(lt (mult (S r) p) (mult (S r) q)).
Proof.
   Intros p q H.
   Induction r.
   Simpl.
   Rewrite <- plus_n_O.
   Rewrite <- plus_n_O.
   Assumption.
   Intros r1 IHr1.
   Simpl.
   Apply lt_plus_plus.
   Assumption.
   Assumption.
Qed.


Lemma le_mult_r: (p,q:nat)(le p q)->(r:nat)(le (mult p r) (mult q r)).
Proof.
   Intros p q H.
   Induction r.
   Simpl.
   Rewrite <- (mult_n_O p).
   Rewrite <- (mult_n_O q).
   Apply le_n.
   Intros r1 IHr1.
   Rewrite <- (mult_n_Sm p r1).
   Rewrite <- (mult_n_Sm q r1).
   Apply le_plus_plus.
   Assumption.
   Assumption.
Qed.

Lemma sqrbound: (p,q:nat)(le (mult p p) (mult p q)) \/
                                            (le (mult q q) (mult p q)).
Proof.
   Intros.
   Elim (le_or_lt p q).
   Left.
   Apply le_mult_l.
   Assumption.
   Right.
   Apply le_mult_r.
   Apply lt_le_weak.
   Assumption.
Qed.

Lemma le_n_nm: (n,m:nat)(le n (mult n (S m))).
Proof.
   Induction n.
   Simpl.
   Intros.
   Apply le_n.
   Intros n1 IHn1.
   Simpl.
   Intros.
   Apply le_n_S.
   Rewrite (plus_sym m (mult n1 (S m))).
   Apply le_plus_trans.
   Apply IHn1.
Qed.

Lemma le_n_mn: (n,m:nat)(le n (mult (S m) n)).
Proof.
   Intros.
   Rewrite (mult_sym (S m) n).
   Apply le_n_nm.
Qed.

Lemma le_n_nn: (n:nat)(le n (mult n n)).
Proof.
   Intro n. Case n.
   Simpl. Apply le_n.
   Simpl. Intros. Apply le_n_S. Apply le_plus_trans. Apply le_n.
Qed.

Lemma lt_n_nm: (n,m:nat)(lt O n)->(lt (1) m)->(lt n (mult n m)). 
Proof.
   Intros n m.
   Case n. Intros. Elim (lt_n_O O). Assumption.
   Intro n1. Case m. Intros. Elim (lt_n_O (1)). Assumption.
   Intro m1. Case m1. Intros. Elim (lt_n_n (1)). Assumption.
   Intro m2. Elim n1.
   Simpl. Intros. Apply lt_n_S. Apply lt_O_Sn.
   Simpl. Intros n2 IH. Intros.
   Apply lt_n_S.
   Apply lt_trans with (S (S (plus m2 (mult n2 (S (S m2)))))).
   Apply IH.
   Apply lt_O_Sn.
   Apply lt_n_S.
   Apply lt_O_Sn.
   Apply lt_n_S.
   Rewrite (plus_sym m2).
   Rewrite (plus_sym m2).
   Simpl.
   Apply lt_n_S.
   Apply lt_le_trans with (S (plus (mult n2 (S (S m2))) m2)).
   Apply lt_n_Sn.
   Apply le_n_S.
   Apply le_plus_trans.
   Apply le_n.
Qed.

Lemma sqr_ascend: (n:nat)(gt n (1)) -> (lt n (mult n n)).
Proof.
   Induction n.
   Intros.
   Elim (lt_n_O (1)).
   Assumption.
   Intros m IHm.
   Intro.
   Unfold gt in H.
   Unfold lt in H.
   Elim (le_lt_or_eq (1) m).
   Intros.
   Simpl.
   Apply lt_n_S.
   Rewrite <- (mult_n_Sm m m).
   Rewrite plus_sym.
   Apply lt_plus_trans.
   Apply lt_plus_trans.
   Apply IHm.
   Assumption.
   Intros.
   Rewrite <- H0.
   Simpl.
   Unfold lt.
   Apply le_S.
   Apply le_n.
   Apply le_S_n.
   Assumption.
Qed.

Lemma witness_le: (x,y:nat)(EX q:nat | (plus x q)=y)->(le x y).
Proof.
   Intros. Elim H. Intro q. Intros.
   Rewrite <- H0.
   Elim q.
   Rewrite <- plus_n_O. Apply le_n.
   Intros. Rewrite <- plus_n_Sm. Apply le_S. Assumption.
Qed.

Lemma le_witness: (x,y:nat)(le x y)->(EX q:nat | (plus x q)=y).
Proof.
   Intros x y.
   Intro.
   Elim H.
   Split with O.
   Simpl.
   Symmetry.
   Apply plus_n_O.
   Intros.
   Case H1.
   Intros.
   Split with (S x0).
   Replace (plus x (S x0)) with (S (plus x x0)).
   Simpl.
   Rewrite H2.
   Reflexivity.
   Apply plus_n_Sm.
Qed.

Lemma lt_witness: (x,y:nat)(lt x y)->(EX q:nat | (plus x q)=y /\ (lt O q)).
Proof.
   Unfold lt.
   Intros.
   Elim (le_witness (S x) y).
   Intros.
   Split with (S x0).
   Split.
   Rewrite <- plus_n_Sm.
   Assumption.
   Apply le_n_S.
   Apply le_O_n.
   Assumption.
Qed.


Lemma le_le_mult:
   (b,a,c,d:nat)(le a b) -> (le c d) -> (le (mult a c) (mult b d)).
Proof.
   Induction b.
   Intros.
   Replace a with O.
   Simpl.
   Apply le_n.
   Apply le_n_O_eq.
   Assumption.
   Intros b1 IHb1.
   Simpl.
   Intros.
   Elim (le_lt_or_eq a (S b1)).
   Unfold lt.
   Intros.
   Rewrite (plus_sym d (mult b1 d)).
   Apply le_plus_trans.
   Apply IHb1.
   Apply le_S_n.
   Assumption.
   Assumption.
   Intro.
   Rewrite H1.
   Replace (plus d (mult b1 d)) with (mult (S b1) d).
   Apply le_mult_l.
   Assumption.
   Reflexivity.
   Assumption.
Qed.

Lemma lt_lt_mult:
   (a,b,c,d:nat)(lt a b) -> (lt c d) -> (lt (mult a c) (mult b d)).
Proof.
   Unfold lt.
   Intros.
   Apply le_trans with (mult (S a) (S c)).
   Simpl.
   Apply le_n_S.
   Rewrite <- (mult_n_Sm a c).
   Rewrite (plus_sym c (plus (mult a c) a)).
   Apply le_plus_trans.
   Apply le_plus_trans.
   Apply le_n.
   Apply le_le_mult.
   Assumption.
   Assumption.
Qed.

Lemma lt_n_nm_m_gt_1:
   (a,b:nat)(lt a (mult a b))->(gt b (1)).
Proof.
   Intros a b. Case b.
   Rewrite <- (mult_n_O a). Intro. Elim (lt_n_O a). Assumption.
   Intro b1. Case b1.
   Rewrite <- (mult_n_Sm a O).
   Rewrite <- (mult_n_O a). Simpl. Intro.
   Elim (lt_n_n a). Assumption.
   Intros. Apply gt_n_S. Apply gt_Sn_O.
Qed.

Lemma n0n1_or_gt: (n:nat)n=O\/n=(1)\/(gt n (1)).
Proof.
   Intro n. Case n.
   Left. Reflexivity.
   Intro n1. Case n1.
   Right. Left. Reflexivity.
   Intro n2.
   Right. Right. Apply gt_n_S. Apply gt_Sn_O.
Qed.

Lemma lt_multpred_pp:
    (p:nat)(gt p (1))->(lt (mult (pred p) (pred p)) (mult p p)).
Proof.
   Intro.
   Case p.
   Intro.
   Elim (lt_n_O (1)).
   Assumption.
   Intro p1.
   Case p1.
   Intro.
   Elim (lt_n_n (1)).
   Assumption.
   Intro p2.
   Intros.
   Apply lt_lt_mult.
   Simpl. Apply lt_n_Sn.
   Simpl. Apply lt_n_Sn.
Qed.

Lemma le_diff0: (b,a,c:nat)(le a b)->a=(plus b c)->c=(0).
Proof.
   Induction b.
   Simpl. Intro.
   Case a.
   Intros.
   Rewrite H0.
   Reflexivity.
   Intros.
   Elim (lt_n_O n).
   Assumption.
   Intros b1 IH.
   Simpl.
   Intros.
   Rewrite H0 in H.
   Apply (IH (plus b1 c) c).
   Apply le_S_n.
   Assumption.
   Reflexivity.
Qed.

Lemma simpl_lt_mult_l:
   (a,b,c:nat)
   (lt (mult a b) (mult a c)) -> (lt b c).
Proof.
   Induction a.
   Simpl.
   Intros.
   Elim (lt_n_n O).
   Assumption.
   Intros a1 IH.
   Intros.
   Elim (le_or_lt b c).
   Intro.
   Elim (le_lt_or_eq b c).
   Intro.
   Assumption.
   Intros.
   Rewrite H1 in H.
   Elim (lt_n_n (mult (S a1) c)).
   Assumption.
   Assumption.
   Intros.
   Cut (le (mult (S a1) c) (mult (S a1) b)).
   Intros.
   Elim (le_not_lt (mult (S a1) c) (mult (S a1) b)).
   Assumption.
   Assumption.
   Apply lt_le_weak.
   Apply lt_mult_l.
   Assumption.
Qed.

Lemma simpl_le_mult_l:
   (a,b,c:nat)
      (lt O a)->(le (mult a b) (mult a c)) -> (le b c).
Proof.
   Induction a.
   Intros.
   Elim (lt_n_O O).
   Assumption.
   Intros a1 IH.
   Intros.
   Simpl in H0.
   Elim (le_or_lt b c).
   Intro.
   Assumption.
   Intro.
   Elim (lt_not_le (mult (S a1) c) (mult (S a1) b)).
   Apply lt_mult_l.
   Assumption.
   Assumption.
Qed.

Lemma simpl_eq_mult_l: (a,b,c:nat)(lt O a)->(mult a b)=(mult a c)->b=c.
Proof.
   Intros. Apply le_antisym.
   Apply simpl_le_mult_l with a. Assumption. Rewrite H0. Apply le_n.
   Apply simpl_le_mult_l with a. Assumption. Rewrite H0. Apply le_n.
Qed.

Lemma mult_ppq_p0q1: (p,q:nat)p=(mult p q)->p=O\/q=(1).
Proof.
   Intro p. Case p. Left. Reflexivity.
   Intro p1. Right.
   Apply simpl_eq_mult_l with (S p1). Apply lt_O_Sn.
   Rewrite <- H.
   Rewrite <- mult_n_Sm. Rewrite <- mult_n_O.
   Simpl. Reflexivity.
Qed.

Lemma mult_pq1_p1q1: (p,q:nat)(mult p q)=(1) -> p=(1)/\q=(1).
Proof.
   Intro p. Case p. Simpl. Intros. Discriminate H.
   Intro p1. Case p1. Simpl.
   Intro q. Rewrite <- plus_n_O. Split. Reflexivity. Assumption.
   Intro p2.
   Intro q. Case q. Rewrite <- mult_n_O. Intro. Discriminate H.
   Intro q1. Case q1.
   Rewrite <- mult_n_Sm.
   Rewrite <- mult_n_O.
   Simpl. Intro. Discriminate H.
   Intro q2. Simpl. Intro. Discriminate H.
Qed.

Lemma Zmult_ab0a0b0: (a,b:Z)`a*b=0`->`a=0`\/`b=0`.
Proof.
   Induction a.
   Simpl. Left. Reflexivity.
   Intro p. Induction b.
   Simpl. Right. Reflexivity.
   Simpl. Intros. Discriminate H.
   Simpl. Intros. Discriminate H.
   Intro. Induction b.
   Simpl. Right. Reflexivity.
   Simpl. Intros. Discriminate H.
   Simpl. Intros. Discriminate H.
Qed.

Lemma Zle_minus: (a,b:Z)`b<=a`->`0<=a-b`.
Proof.
   Intros a b. Intros.
   Apply Zsimpl_le_plus_l with b.
   Unfold Zminus. Rewrite (Zplus_sym a).
   Rewrite (Zplus_assoc_l b `-b`). Rewrite Zplus_inverse_r.
   Simpl. Rewrite <- Zplus_n_O. Assumption.
Qed.

Lemma Zopp_lt_gt_0: (x:Z)`x < 0`->`(-x) > 0`.
Proof.
   Induction x.
   Intro. Unfold Zlt in H. Simpl in H. Discriminate H.
   Intros. Unfold Zlt in H. Simpl in H. Discriminate H.
   Intros. Simpl. Unfold Zgt. Simpl. Reflexivity.
Qed.

Lemma Zlt_neq: (x,y:Z)`x<y`->`x<>y`.
Proof.
   Intros. Intro.
   Rewrite H0 in H.
   Elim (Zlt_n_n y).
   Assumption.
Qed.

Lemma Zgt_neq: (x,y:Z)`x>y`->`x<>y`.
Proof.
   Intros. Intro.
   Rewrite H0 in H.
   Elim (Zlt_n_n y).
   Apply Zgt_lt. Assumption.
Qed.