diff options
author | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
---|---|---|
committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-09-17 15:58:14 +0000 |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /theories/NArith/BinNat.v | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith/BinNat.v')
-rw-r--r-- | theories/NArith/BinNat.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v index eaf3f126a..e02f2817c 100644 --- a/theories/NArith/BinNat.v +++ b/theories/NArith/BinNat.v @@ -45,7 +45,7 @@ Definition Ndouble_plus_one x := (** Operation x -> 2*x *) -Definition Ndouble n := +Definition Ndouble n := match n with | N0 => N0 | Npos p => Npos (xO p) @@ -130,12 +130,12 @@ Infix ">" := Ngt : N_scope. (** Min and max *) -Definition Nmin (n n' : N) := match Ncompare n n' with +Definition Nmin (n n' : N) := match Ncompare n n' with | Lt | Eq => n | Gt => n' end. -Definition Nmax (n n' : N) := match Ncompare n n' with +Definition Nmax (n n' : N) := match Ncompare n n' with | Lt | Eq => n' | Gt => n end. @@ -149,7 +149,7 @@ Lemma N_ind_double : (forall a, P a -> P (Ndouble_plus_one a)) -> P a. Proof. intros; elim a. trivial. - simple induction p. intros. + simple induction p. intros. apply (H1 (Npos p0)); trivial. intros; apply (H0 (Npos p0)); trivial. intros; apply (H1 N0); assumption. @@ -162,7 +162,7 @@ Lemma N_rec_double : (forall a, P a -> P (Ndouble_plus_one a)) -> P a. Proof. intros; elim a. trivial. - simple induction p. intros. + simple induction p. intros. apply (H1 (Npos p0)); trivial. intros; apply (H0 (Npos p0)); trivial. intros; apply (H1 N0); assumption. @@ -354,7 +354,7 @@ destruct p; intros Hp H. contradiction Hp; reflexivity. destruct n; destruct m; reflexivity || (try discriminate H). injection H; clear H; intro H; rewrite Pmult_reg_r with (1 := H); reflexivity. -Qed. +Qed. (** Properties of comparison *) @@ -373,7 +373,7 @@ Qed. Theorem Ncompare_eq_correct : forall n m:N, (n ?= m) = Eq <-> n = m. Proof. -split; intros; +split; intros; [ apply Ncompare_Eq_eq; auto | subst; apply Ncompare_refl ]. Qed. |