diff options
Diffstat (limited to 'theories/Sets/Integers.v')
| -rw-r--r-- | theories/Sets/Integers.v | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/theories/Sets/Integers.v b/theories/Sets/Integers.v index 1786edf1..15c1b665 100644 --- a/theories/Sets/Integers.v +++ b/theories/Sets/Integers.v @@ -24,7 +24,7 @@ (* in Summer 1995. Several developments by E. Ledinot were an inspiration. *) (****************************************************************************) -(*i $Id: Integers.v 10637 2008-03-07 23:52:56Z letouzey $ i*) +(*i $Id$ i*) Require Export Finite_sets. Require Export Constructive_sets. @@ -45,7 +45,7 @@ Require Export Partial_Order. Require Export Cpo. Section Integers_sect. - + Inductive Integers : Ensemble nat := Integers_defn : forall x:nat, In nat Integers x. @@ -53,7 +53,7 @@ Section Integers_sect. Proof. red in |- *; auto with arith. Qed. - + Lemma le_antisym : Antisymmetric nat le. Proof. red in |- *; intros x y H H'; rewrite (le_antisym x y); auto. @@ -63,12 +63,12 @@ Section Integers_sect. Proof. red in |- *; intros; apply le_trans with y; auto. Qed. - + Lemma le_Order : Order nat le. Proof. - split; [exact le_reflexive | exact le_trans | exact le_antisym]. + split; [exact le_reflexive | exact le_trans | exact le_antisym]. Qed. - + Lemma triv_nat : forall n:nat, In nat Integers n. Proof. exact Integers_defn. @@ -77,11 +77,11 @@ Section Integers_sect. Definition nat_po : PO nat. apply Definition_of_PO with (Carrier_of := Integers) (Rel_of := le); auto with sets arith. - apply Inhabited_intro with (x := 0). + apply Inhabited_intro with (x := 0). apply Integers_defn. - exact le_Order. + exact le_Order. Defined. - + Lemma le_total_order : Totally_ordered nat nat_po Integers. Proof. apply Totally_ordered_definition. @@ -92,7 +92,7 @@ Section Integers_sect. intro H'1; right. cut (y <= x); auto with sets arith. Qed. - + Lemma Finite_subset_has_lub : forall X:Ensemble nat, Finite nat X -> exists m : nat, Upper_Bound nat nat_po X m. @@ -124,7 +124,7 @@ Section Integers_sect. apply H'4 with (y := x0). elim H'3; simpl in |- *; auto with sets arith. trivial. intros x1 H'4; elim H'4. unfold nat_po; simpl; trivial. exists x0. - apply Upper_Bound_definition. + apply Upper_Bound_definition. unfold nat_po. simpl. apply triv_nat. intros y H'1; elim H'1. intros x1 H'4; try assumption. @@ -148,7 +148,7 @@ Section Integers_sect. absurd (S x <= x); auto with arith. apply triv_nat. Qed. - + Lemma Integers_infinite : ~ Finite nat Integers. Proof. generalize Integers_has_no_ub. |