diff options
Diffstat (limited to 'theories/Numbers/Natural')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NIso.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NMinus.v | 16 | ||||
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 4 |
3 files changed, 12 insertions, 12 deletions
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v index 10c341cbfa..4df46e20eb 100644 --- a/theories/Numbers/Natural/Abstract/NIso.v +++ b/theories/Numbers/Natural/Abstract/NIso.v @@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ : forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n). Proof. unfold natural_isomorphism. -intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq); -[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |]. +intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ; +[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd]. Qed. Theorem hom_nat_iso : homomorphism natural_isomorphism. diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v index faf4759bdb..5e1d5d8c3c 100644 --- a/theories/Numbers/Natural/Abstract/NMinus.v +++ b/theories/Numbers/Natural/Abstract/NMinus.v @@ -63,8 +63,8 @@ Proof. intros n m p; induct p. intro; now do 2 rewrite minus_0_r. intros p IH H. do 2 rewrite minus_succ_r. -rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |]. -rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l. +rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l). +rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l). reflexivity. Qed. @@ -76,13 +76,13 @@ Qed. Theorem plus_minus : forall n m : N, (n + m) - m == n. Proof. -intros n m. rewrite <- plus_minus_assoc. apply le_refl. +intros n m. rewrite <- plus_minus_assoc by (apply le_refl). rewrite minus_diag; now rewrite plus_0_r. Qed. Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m. Proof. -intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |]. +intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption. rewrite plus_comm. apply plus_minus. Qed. @@ -121,7 +121,7 @@ Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m. Proof. intros n m p H. rewrite (plus_comm n m). -rewrite <- plus_minus_assoc; [assumption |]. +rewrite <- plus_minus_assoc by assumption. now rewrite (plus_comm m (n - p)). Qed. @@ -151,8 +151,8 @@ Proof. intros n m; cases m. now rewrite pred_0, times_0_r, minus_0_l. intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc. -now apply eq_le_incl. now rewrite minus_diag, plus_0_r. +now apply eq_le_incl. Qed. Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p. @@ -160,9 +160,9 @@ Proof. intros n m p; induct n. now rewrite minus_0_l, times_0_l, minus_0_l. intros n IH. destruct (le_gt_cases m n) as [H | H]. -rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l. +rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l. rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p). -rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |]. +rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r. now apply <- plus_cancel_l. assert (H1 : S n <= m); [now apply <- le_succ_l |]. setoid_replace (S n - m) with 0 by now apply <- minus_0_le. diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 7b4645be35..1e53d80637 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -506,7 +506,7 @@ Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m). Proof. intros n m H1; split; intro H2. assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n. -now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2; +now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; [apply <- succ_lt_mono | | |]. assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). apply lt_le_trans with (P m). assumption. apply le_pred_l. @@ -515,7 +515,7 @@ Qed. Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m. Proof. -intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ. +intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ. Qed. Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) |