diff options
Diffstat (limited to 'theories/Arith/Euclid.v')
| -rw-r--r-- | theories/Arith/Euclid.v | 85 |
1 files changed, 44 insertions, 41 deletions
diff --git a/theories/Arith/Euclid.v b/theories/Arith/Euclid.v index 23bc7cdb..3d6f1af5 100644 --- a/theories/Arith/Euclid.v +++ b/theories/Arith/Euclid.v @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Euclid.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Euclid.v 9245 2006-10-17 12:53:34Z notin $ i*) Require Import Mult. Require Import Compare_dec. @@ -17,52 +17,55 @@ Open Local Scope nat_scope. Implicit Types a b n q r : nat. Inductive diveucl a b : Set := - divex : forall q r, b > r -> a = q * b + r -> diveucl a b. + divex : forall q r, b > r -> a = q * b + r -> diveucl a b. Lemma eucl_dev : forall n, n > 0 -> forall m:nat, diveucl m n. -intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. -elim (le_gt_dec b n). -intro lebn. -elim (H0 (n - b)); auto with arith. -intros q r g e. -apply divex with (S q) r; simpl in |- *; auto with arith. -elim plus_assoc. -elim e; auto with arith. -intros gtbn. -apply divex with 0 n; simpl in |- *; auto with arith. +Proof. + intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. + elim (le_gt_dec b n). + intro lebn. + elim (H0 (n - b)); auto with arith. + intros q r g e. + apply divex with (S q) r; simpl in |- *; auto with arith. + elim plus_assoc. + elim e; auto with arith. + intros gtbn. + apply divex with 0 n; simpl in |- *; auto with arith. Qed. Lemma quotient : - forall n, - n > 0 -> - forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}. -intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. -elim (le_gt_dec b n). -intro lebn. -elim (H0 (n - b)); auto with arith. -intros q Hq; exists (S q). -elim Hq; intros r Hr. -exists r; simpl in |- *; elim Hr; intros. -elim plus_assoc. -elim H1; auto with arith. -intros gtbn. -exists 0; exists n; simpl in |- *; auto with arith. + forall n, + n > 0 -> + forall m:nat, {q : nat | exists r : nat, m = q * n + r /\ n > r}. +Proof. + intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. + elim (le_gt_dec b n). + intro lebn. + elim (H0 (n - b)); auto with arith. + intros q Hq; exists (S q). + elim Hq; intros r Hr. + exists r; simpl in |- *; elim Hr; intros. + elim plus_assoc. + elim H1; auto with arith. + intros gtbn. + exists 0; exists n; simpl in |- *; auto with arith. Qed. Lemma modulo : - forall n, - n > 0 -> - forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}. -intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. -elim (le_gt_dec b n). -intro lebn. -elim (H0 (n - b)); auto with arith. -intros r Hr; exists r. -elim Hr; intros q Hq. -elim Hq; intros; exists (S q); simpl in |- *. -elim plus_assoc. -elim H1; auto with arith. -intros gtbn. -exists n; exists 0; simpl in |- *; auto with arith. -Qed.
\ No newline at end of file + forall n, + n > 0 -> + forall m:nat, {r : nat | exists q : nat, m = q * n + r /\ n > r}. +Proof. + intros b H a; pattern a in |- *; apply gt_wf_rec; intros n H0. + elim (le_gt_dec b n). + intro lebn. + elim (H0 (n - b)); auto with arith. + intros r Hr; exists r. + elim Hr; intros q Hq. + elim Hq; intros; exists (S q); simpl in |- *. + elim plus_assoc. + elim H1; auto with arith. + intros gtbn. + exists n; exists 0; simpl in |- *; auto with arith. +Qed. |