5 files changed, 35 insertions, 14 deletions
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 9b1bca7c4..a0ba5127d 100755
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -64,7 +64,7 @@ Fixpoint  beq_nat [n:nat] : nat -> bool :=
 
 Lemma beq_nat_refl : (x:nat)true=(beq_nat x x).
 Proof.
-  NewInduction x; Simpl; Auto.
+  Intro x; NewInduction x; Simpl; Auto.
 Qed.
 
 Definition beq_nat_eq : (x,y:nat)true=(beq_nat x y)->x=y.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index c8e9a5d40..658c25194 100755
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -35,7 +35,7 @@ Qed.
 Hints Resolve minus_Sn_m : arith v62.
 
 Theorem pred_of_minus : (x:nat)(pred x)=(minus x (S O)).
-NewInduction x; Simpl; Auto with arith.
+Intro x; NewInduction x; Simpl; Auto with arith.
 Qed.
 
 (** Diagonal *)
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index f56ee2f60..7c8f43f82 100755
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -91,7 +91,7 @@ Hints Resolve mult_O_le : arith v62.
 
 Lemma mult_le : (m,n,p:nat) (le n p) -> (le (mult m n) (mult m p)).
 Proof.
-  NewInduction m. Intros. Simpl. Apply le_n.
+  Intro m; NewInduction m. Intros. Simpl. Apply le_n.
   Intros. Simpl. Apply le_plus_plus. Assumption.
   Apply IHm. Assumption.
 Qed.
@@ -122,7 +122,7 @@ Qed.
 
 Lemma mult_lt : (m,n,p:nat) (lt n p) -> (lt (mult (S m) n) (mult (S m) p)).
 Proof.
-  NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
+  Intro m; NewInduction m. Intros. Simpl. Rewrite <- plus_n_O. Rewrite <- plus_n_O. Assumption.
   Intros. Exact (lt_plus_plus ? ? ? ? H (IHm ? ? H)).
 Qed.
 
@@ -145,12 +145,33 @@ Qed.
 
 Lemma mult_le_conv_1 : (m,n,p:nat) (le (mult (S m) n) (mult (S m) p)) -> (le n p).
 Proof.
-  Intros. Elim (le_or_lt n p). Trivial.
+  Intros m n p H. Elim (le_or_lt n p). Trivial.
   Intro H0. Cut (lt (mult (S m) n) (mult (S m) n)). Intro. Elim (lt_n_n ? H1).
   Apply le_lt_trans with m:=(mult (S m) p). Assumption.
   Apply mult_lt. Assumption.
 Qed.
 
+(** n|->2*n and n|->2n+1 have disjoint image *)
+
+V7only [ (* From Zdivides *) ].
+Theorem odd_even_lem:
+  (p, q : ?)  ~ (plus (mult (2) p) (1)) = (mult (2) q).
+Intros p; Elim p; Auto.
+Intros q; Case q; Simpl.
+Red; Intros; Discriminate.
+Intros q'; Rewrite [x, y : ?]  (plus_sym x (S y)); Simpl; Red; Intros;
+ Discriminate.
+Intros p' H q; Case q.
+Simpl; Red; Intros; Discriminate.
+Intros q'; Red; Intros H0; Case (H q').
+Replace (mult (S (S O)) q') with (minus (mult (S (S O)) (S q')) (2)).
+Rewrite <- H0; Simpl; Auto.
+Repeat Rewrite [x, y : ?]  (plus_sym x (S y)); Simpl; Auto.
+Simpl; Repeat Rewrite [x, y : ?]  (plus_sym x (S y)); Simpl; Auto.
+Case q'; Simpl; Auto.
+Qed.
+
+
 (** Tail-recursive mult *)
 
 (** [tail_mult] is an alternative definition for [mult] which is 
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index d73b9820d..d44914499 100755
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -61,11 +61,9 @@ Proof.
 NewInduction n ; Simpl ; Auto with arith.
 Qed.
 
-(** Relations with order *)
-
 Lemma simpl_le_plus_l : (p,n,m:nat) (p+n)<=(p+m) -> n<=m.
 Proof.
-NewInduction p; Simpl; Auto with arith.
+Intro p; NewInduction p; Simpl; Auto with arith.
 Qed.
 
 Lemma simpl_lt_plus_l : (n,m,p:nat) (p+n)<(p+m) -> n<m.
@@ -73,6 +71,8 @@ Proof.
 NewInduction p; Simpl; Auto with arith.
 Qed.
 
+(** Compatibility with order *)
+
 Lemma le_reg_l : (n,m,p:nat) n<=m -> (p+n)<=(p+m).
 Proof.
 NewInduction p; Simpl; Auto with arith.
@@ -149,14 +149,14 @@ Qed.
 
 Lemma plus_is_O : (m,n:nat) (m+n)=O -> m=O /\ n=O.
 Proof.
-  NewDestruct m; Auto.
+  Intro m; NewDestruct m; Auto.
   Intros. Discriminate H.
 Qed.
 
 Definition plus_is_one : 
       (m,n:nat) (m+n)=(S O) -> {m=O /\ n=(S O)}+{m=(S O) /\ n=O}.
 Proof.
-  NewDestruct m; Auto.
+  Intro m; NewDestruct m; Auto.
   NewDestruct n; Auto.
   Intros. 
   Simpl in H. Discriminate H.
@@ -166,7 +166,7 @@ Defined.
 
 Lemma plus_permute_2_in_4 : (m,n,p,q:nat) ((m+n)+(p+q))=((m+p)+(n+q)).
 Proof.
-  Intros. 
+  Intros m n p q. 
   Rewrite <- (plus_assoc_l m n (p+q)). Rewrite (plus_assoc_l n p q).
   Rewrite (plus_sym n p). Rewrite <- (plus_assoc_l p n q). Apply plus_assoc_l.
 Qed.
diff --git a/theories/Arith/Wf_nat.v b/theories/Arith/Wf_nat.v
index e87f436ed..51df19b29 100755
--- a/theories/Arith/Wf_nat.v
+++ b/theories/Arith/Wf_nat.v
@@ -133,7 +133,7 @@ Defined.
 
 Lemma lt_wf_ind : (p:nat)(P:nat->Prop)
               ((n:nat)((m:nat)(lt m n)->(P m))->(P n)) -> (P p).
-Intros; Elim (lt_wf p); Auto with arith.
+Intro p; Intros; Elim (lt_wf p); Auto with arith.
 Qed.
 
 Lemma gt_wf_rec : (p:nat)(P:nat->Set)
@@ -151,7 +151,7 @@ Lemma lt_wf_double_rec :
   ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
    -> (p,q:nat)(P p q).
 Intros P Hrec p; Pattern p; Apply lt_wf_rec.
-Intros; Pattern q; Apply lt_wf_rec; Auto with arith.
+Intros n H q; Pattern q; Apply lt_wf_rec; Auto with arith.
 Defined.
 
 Lemma lt_wf_double_ind : 
@@ -159,7 +159,7 @@ Lemma lt_wf_double_ind :
   ((n,m:nat)((p,q:nat)(lt p n)->(P p q))->((p:nat)(lt p m)->(P n p))->(P n m))
    -> (p,q:nat)(P p q).
 Intros P Hrec p; Pattern p; Apply lt_wf_ind.
-Intros; Pattern q; Apply lt_wf_ind; Auto with arith.
+Intros n H q; Pattern q; Apply lt_wf_ind; Auto with arith.
 Qed.
 
 Hints Resolve lt_wf : arith.