diff options
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZAdd.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZBase.v | 4 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 50 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZGcd.v | 10 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZLog.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMul.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZMulOrder.v | 8 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZOrder.v | 18 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZParity.v | 14 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZPow.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 6 |
11 files changed, 62 insertions, 62 deletions
diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v index 7982411bdd..66cbba9e08 100644 --- a/theories/Numbers/NatInt/NZAdd.v +++ b/theories/Numbers/NatInt/NZAdd.v @@ -22,7 +22,7 @@ Ltac nzsimpl' := autorewrite with nz nz'. Theorem add_0_r : forall n, n + 0 == n. Proof. - nzinduct n. + intro n; nzinduct n. - now nzsimpl. - intro. nzsimpl. now rewrite succ_inj_wd. Qed. diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v index 8bc393bbad..d4f70adbc5 100644 --- a/theories/Numbers/NatInt/NZBase.v +++ b/theories/Numbers/NatInt/NZBase.v @@ -74,7 +74,7 @@ Proof. intros z Base Step; revert Base; pattern z; apply bi_induction. - solve_proper. - intro; now apply bi_induction. -- intro; pose proof (Step n); tauto. +- intro n; pose proof (Step n); tauto. Qed. End CentralInduction. @@ -83,7 +83,7 @@ Tactic Notation "nzinduct" ident(n) := induction_maker n ltac:(apply bi_induction). Tactic Notation "nzinduct" ident(n) constr(u) := - induction_maker n ltac:(apply central_induction with (z := u)). + induction_maker n ltac:(apply (fun A A_wd => central_induction A A_wd u)). End NZBaseProp. diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 1c45aa440f..e6249be8df 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -116,7 +116,7 @@ Qed. Theorem div_small: forall a b, 0<=a<b -> a/b == 0. Proof. -intros. symmetry. +intros a b ?. symmetry. apply div_unique with a; intuition; try order. now nzsimpl. Qed. @@ -149,7 +149,7 @@ Qed. Lemma mod_1_r: forall a, 0<=a -> a mod 1 == 0. Proof. -intros. symmetry. +intros a ?. symmetry. apply mod_unique with a; try split; try order; try apply lt_0_1. now nzsimpl. Qed. @@ -173,7 +173,7 @@ Qed. Lemma mod_mul : forall a b, 0<=a -> 0<b -> (a*b) mod b == 0. Proof. -intros; symmetry. +intros a b ? ?; symmetry. apply mod_unique with a; try split; try order. - apply mul_nonneg_nonneg; order. - nzsimpl; apply mul_comm. @@ -186,7 +186,7 @@ Qed. Theorem mod_le: forall a b, 0<=a -> 0<b -> a mod b <= a. Proof. -intros. destruct (le_gt_cases b a). +intros a b ? ?. destruct (le_gt_cases b a). - apply le_trans with b; auto. apply lt_le_incl. destruct (mod_bound_pos a b); auto. - rewrite lt_eq_cases; right. @@ -198,7 +198,7 @@ Qed. Lemma div_pos: forall a b, 0<=a -> 0<b -> 0 <= a/b. Proof. -intros. +intros a b ? ?. rewrite (mul_le_mono_pos_l _ _ b); auto; nzsimpl. rewrite (add_le_mono_r _ _ (a mod b)). rewrite <- div_mod by order. @@ -247,7 +247,7 @@ Qed. Lemma div_lt : forall a b, 0<a -> 1<b -> a/b < a. Proof. -intros. +intros a b ? ?. assert (0 < b) by (apply lt_trans with 1; auto using lt_0_1). destruct (lt_ge_cases a b). - rewrite div_small; try split; order. @@ -284,7 +284,7 @@ Qed. Lemma mul_div_le : forall a b, 0<=a -> 0<b -> b*(a/b) <= a. Proof. -intros. +intros a b ? ?. rewrite (add_le_mono_r _ _ (a mod b)), <- div_mod by order. rewrite <- (add_0_r a) at 1. rewrite <- add_le_mono_l. destruct (mod_bound_pos a b); order. @@ -292,7 +292,7 @@ Qed. Lemma mul_succ_div_gt : forall a b, 0<=a -> 0<b -> a < b*(S (a/b)). Proof. -intros. +intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite (mul_succ_r). rewrite <- add_lt_mono_l. @@ -304,7 +304,7 @@ Qed. Lemma div_exact : forall a b, 0<=a -> 0<b -> (a == b*(a/b) <-> a mod b == 0). Proof. -intros. rewrite (div_mod a b) at 1 by order. +intros a b ? ?. rewrite (div_mod a b) at 1 by order. rewrite <- (add_0_r (b*(a/b))) at 2. apply add_cancel_l. Qed. @@ -314,7 +314,7 @@ Qed. Theorem div_lt_upper_bound: forall a b q, 0<=a -> 0<b -> a < b*q -> a/b < q. Proof. -intros. +intros a b q ? ? ?. rewrite (mul_lt_mono_pos_l b) by order. apply le_lt_trans with a; auto. apply mul_div_le; auto. @@ -323,7 +323,7 @@ Qed. Theorem div_le_upper_bound: forall a b q, 0<=a -> 0<b -> a <= b*q -> a/b <= q. Proof. -intros. +intros a b q ? ? ?. rewrite (mul_le_mono_pos_l _ _ b) by order. apply le_trans with a; auto. apply mul_div_le; auto. @@ -362,7 +362,7 @@ Qed. Lemma mod_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) mod c == a mod c. Proof. - intros. + intros a b c ? ? ?. symmetry. apply mod_unique with (a/c+b); auto. - apply mod_bound_pos; auto. @@ -373,7 +373,7 @@ Qed. Lemma div_add : forall a b c, 0<=a -> 0<=a+b*c -> 0<c -> (a + b * c) / c == a / c + b. Proof. - intros. + intros a b c ? ? ?. apply (mul_cancel_l _ _ c); try order. apply (add_cancel_r _ _ ((a+b*c) mod c)). rewrite <- div_mod, mod_add by order. @@ -393,7 +393,7 @@ Qed. Lemma div_mul_cancel_r : forall a b c, 0<=a -> 0<b -> 0<c -> (a*c)/(b*c) == a/b. Proof. - intros. + intros a b c ? ? ?. symmetry. apply div_unique with ((a mod b)*c). - apply mul_nonneg_nonneg; order. @@ -409,13 +409,13 @@ Qed. Lemma div_mul_cancel_l : forall a b c, 0<=a -> 0<b -> 0<c -> (c*a)/(c*b) == a/b. Proof. - intros. rewrite !(mul_comm c); apply div_mul_cancel_r; auto. + intros a b c ? ? ?. rewrite !(mul_comm c); apply div_mul_cancel_r; auto. Qed. Lemma mul_mod_distr_l: forall a b c, 0<=a -> 0<b -> 0<c -> (c*a) mod (c*b) == c * (a mod b). Proof. - intros. + intros a b c ? ? ?. rewrite <- (add_cancel_l _ _ ((c*b)* ((c*a)/(c*b)))). rewrite <- div_mod. - rewrite div_mul_cancel_l; auto. @@ -427,7 +427,7 @@ Qed. Lemma mul_mod_distr_r: forall a b c, 0<=a -> 0<b -> 0<c -> (a*c) mod (b*c) == (a mod b) * c. Proof. - intros. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. + intros a b c ? ? ?. rewrite !(mul_comm _ c); now rewrite mul_mod_distr_l. Qed. (** Operations modulo. *) @@ -435,7 +435,7 @@ Qed. Theorem mod_mod: forall a n, 0<=a -> 0<n -> (a mod n) mod n == a mod n. Proof. - intros. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. + intros a n ? ?. destruct (mod_bound_pos a n); auto. now rewrite mod_small_iff. Qed. Lemma mul_mod_idemp_l : forall a b n, 0<=a -> 0<=b -> 0<n -> @@ -454,13 +454,14 @@ Qed. Lemma mul_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> (a*(b mod n)) mod n == (a*b) mod n. Proof. - intros. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto. + intros a b n ? ? ?. rewrite !(mul_comm a). apply mul_mod_idemp_l; auto. Qed. Theorem mul_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a * b) mod n == ((a mod n) * (b mod n)) mod n. Proof. - intros. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. - reflexivity. + intros a b n ? ? ?. rewrite mul_mod_idemp_l, mul_mod_idemp_r; trivial. + - reflexivity. - now destruct (mod_bound_pos b n). Qed. @@ -478,13 +479,14 @@ Qed. Lemma add_mod_idemp_r : forall a b n, 0<=a -> 0<=b -> 0<n -> (a+(b mod n)) mod n == (a+b) mod n. Proof. - intros. rewrite !(add_comm a). apply add_mod_idemp_l; auto. + intros a b n ? ? ?. rewrite !(add_comm a). apply add_mod_idemp_l; auto. Qed. Theorem add_mod: forall a b n, 0<=a -> 0<=b -> 0<n -> (a+b) mod n == (a mod n + b mod n) mod n. Proof. - intros. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. - reflexivity. + intros a b n ? ? ?. rewrite add_mod_idemp_l, add_mod_idemp_r; trivial. + - reflexivity. - now destruct (mod_bound_pos b n). Qed. @@ -525,7 +527,7 @@ Qed. Theorem div_mul_le: forall a b c, 0<=a -> 0<b -> 0<=c -> c*(a/b) <= (c*a)/b. Proof. - intros. + intros a b c ? ? ?. apply div_le_lower_bound; auto. - apply mul_nonneg_nonneg; auto. - rewrite mul_assoc, (mul_comm b c), <- mul_assoc. @@ -538,7 +540,7 @@ Qed. Lemma mod_divides : forall a b, 0<=a -> 0<b -> (a mod b == 0 <-> exists c, a == b*c). Proof. - split. + intros a b ? ?; split. - intros. exists (a/b). rewrite div_exact; auto. - intros (c,Hc). rewrite Hc, mul_comm. apply mod_mul; auto. rewrite (mul_le_mono_pos_l _ _ b); auto. nzsimpl. order. diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v index 63cc725aec..c542c3fc2c 100644 --- a/theories/Numbers/NatInt/NZGcd.v +++ b/theories/Numbers/NatInt/NZGcd.v @@ -147,7 +147,7 @@ Qed. Lemma mul_divide_cancel_r : forall n m p, p ~= 0 -> ((n * p | m * p) <-> (n | m)). Proof. - intros. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. + intros n m p ?. rewrite 2 (mul_comm _ p). now apply mul_divide_cancel_l. Qed. Lemma divide_add_r : forall n m p, (n | m) -> (n | p) -> (n | m + p). @@ -215,7 +215,7 @@ Qed. Lemma gcd_divide_iff : forall n m p, (p | gcd n m) <-> (p | n) /\ (p | m). Proof. - intros. split. - split. + intros n m p. split. - split. + transitivity (gcd n m); trivial using gcd_divide_l. + transitivity (gcd n m); trivial using gcd_divide_r. - intros (H,H'). now apply gcd_greatest. @@ -273,18 +273,18 @@ Qed. Lemma gcd_eq_0_l : forall n m, gcd n m == 0 -> n == 0. Proof. - intros. + intros n m H. generalize (gcd_divide_l n m). rewrite H. apply divide_0_l. Qed. Lemma gcd_eq_0_r : forall n m, gcd n m == 0 -> m == 0. Proof. - intros. apply gcd_eq_0_l with n. now rewrite gcd_comm. + intros n m ?. apply gcd_eq_0_l with n. now rewrite gcd_comm. Qed. Lemma gcd_eq_0 : forall n m, gcd n m == 0 <-> n == 0 /\ m == 0. Proof. - intros. split. + intros n m. split. - split. + now apply gcd_eq_0_l with m. + now apply gcd_eq_0_r with n. diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v index 5491d7ab04..526af2f9df 100644 --- a/theories/Numbers/NatInt/NZLog.v +++ b/theories/Numbers/NatInt/NZLog.v @@ -335,7 +335,7 @@ Qed. Lemma log2_succ_or : forall a, log2 (S a) == S (log2 a) \/ log2 (S a) == log2 a. Proof. - intros. + intros a. destruct (le_gt_cases (log2 (S a)) (log2 a)) as [H|H]. - right. generalize (log2_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_succ_le a); order. @@ -601,7 +601,7 @@ Lemma log2_log2_up_exact : Proof. intros a Ha. split. - - intros. exists (log2 a). + - intros H. exists (log2 a). generalize (log2_log2_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b,Hb). rewrite Hb. @@ -806,8 +806,8 @@ Qed. Lemma log2_up_succ_or : forall a, log2_up (S a) == S (log2_up a) \/ log2_up (S a) == log2_up a. Proof. - intros. - destruct (le_gt_cases (log2_up (S a)) (log2_up a)). + intros a. + destruct (le_gt_cases (log2_up (S a)) (log2_up a)) as [H|H]. - right. generalize (log2_up_le_mono _ _ (le_succ_diag_r a)); order. - left. apply le_succ_l in H. generalize (log2_up_succ_le a); order. Qed. diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v index 9ddf7cb0eb..3d6465191d 100644 --- a/theories/Numbers/NatInt/NZMul.v +++ b/theories/Numbers/NatInt/NZMul.v @@ -17,7 +17,7 @@ Include NZAddProp NZ NZBase. Theorem mul_0_r : forall n, n * 0 == 0. Proof. -nzinduct n; intros; now nzsimpl. +intro n; nzinduct n; intros; now nzsimpl. Qed. Theorem mul_succ_r : forall n m, n * (S m) == n * m + n. diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 46749504a9..c67bbe38d8 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -46,7 +46,7 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. -nzord_induct p. +intro p; nzord_induct p. - order. - intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. - intros p Hp IH n m _. apply le_succ_l in Hp. @@ -196,7 +196,7 @@ Qed. Theorem mul_nonneg_nonneg : forall n m, 0 <= n -> 0 <= m -> 0 <= n*m. Proof. -intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. +intros n m Hn Hm. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. Qed. Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m). @@ -343,7 +343,7 @@ Qed. Lemma square_nonneg : forall a, 0 <= a * a. Proof. - intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). + intro a. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). - now apply mul_le_mono_nonpos_l. - apply mul_le_mono_nonneg_l; order. Qed. @@ -391,7 +391,7 @@ Qed. Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> 2*2*a*b <= (a+b)*(a+b). Proof. - intros. + intros a b Ha Hb. nzsimpl'. rewrite !mul_add_distr_l, !mul_add_distr_r. rewrite (add_comm _ (b*b)), add_assoc. diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v index d576902c5c..68bb974c5d 100644 --- a/theories/Numbers/NatInt/NZOrder.v +++ b/theories/Numbers/NatInt/NZOrder.v @@ -65,7 +65,7 @@ Qed. Theorem le_succ_l : forall n m, S n <= m <-> n < m. Proof. -intro n; nzinduct m n. +intros n m; nzinduct m n. - split; intro H. + false_hyp H nle_succ_diag_l. + false_hyp H lt_irrefl. - intro m. rewrite (lt_eq_cases (S n) (S m)), !lt_succ_r, (lt_eq_cases n m), succ_inj_wd. @@ -362,7 +362,7 @@ induction does not go through, so we need to use strong Lemma lt_exists_pred_strong : forall z n m, z < m -> m <= n -> exists k, m == S k /\ z <= k. Proof. -intro z; nzinduct n z. +intros z n; nzinduct n z. - order. - intro n; split; intros IH m H1 H2. + apply le_succ_r in H2. destruct H2 as [H2 | H2]. @@ -373,7 +373,7 @@ Qed. Theorem lt_exists_pred : forall z n, z < n -> exists k, n == S k /\ z <= k. Proof. -intros z n H; apply lt_exists_pred_strong with (z := z) (n := n). +intros z n H; apply (lt_exists_pred_strong z n). - assumption. - apply le_refl. Qed. @@ -428,12 +428,12 @@ Qed. Lemma A'A_right : (forall n, A' n) -> forall n, z <= n -> A n. Proof. -intros H1 n H2. apply H1 with (n := S n); [assumption | apply lt_succ_diag_r]. +intros H1 n H2. apply (H1 (S n)); [assumption | apply lt_succ_diag_r]. Qed. Theorem strong_right_induction: right_step' -> forall n, z <= n -> A n. Proof. -intro RS'; apply A'A_right; unfold A'; nzinduct n z; +intro RS'; apply A'A_right; unfold A'; intro n; nzinduct n z; [apply rbase | apply rs'_rs''; apply RS']. Qed. @@ -504,7 +504,7 @@ Qed. Theorem strong_left_induction: left_step' -> forall n, n <= z -> A n. Proof. -intro LS'; apply A'A_left; unfold A'; nzinduct n (S z); +intro LS'; apply A'A_left; unfold A'; intro n; nzinduct n (S z); [apply lbase | apply ls'_ls''; apply LS']. Qed. @@ -629,8 +629,7 @@ Qed. Theorem lt_wf : well_founded Rlt. Proof. unfold well_founded. -apply strong_right_induction' with (z := z). -- auto with typeclass_instances. +apply (strong_right_induction' _ _ z). - intros n H; constructor; intros y [H1 H2]. apply nle_gt in H2. elim H2. now apply le_trans with z. - intros n H1 H2; constructor; intros m [H3 H4]. now apply H2. @@ -639,8 +638,7 @@ Qed. Theorem gt_wf : well_founded Rgt. Proof. unfold well_founded. -apply strong_left_induction' with (z := z). -- auto with typeclass_instances. +apply (strong_left_induction' _ _ z). - intros n H; constructor; intros y [H1 H2]. apply nle_gt in H2. + elim H2. diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v index ee6f4014f0..07a33e3f67 100644 --- a/theories/Numbers/NatInt/NZParity.v +++ b/theories/Numbers/NatInt/NZParity.v @@ -47,7 +47,7 @@ Qed. Lemma Even_or_Odd : forall x, Even x \/ Odd x. Proof. - nzinduct x. + intro x; nzinduct x. - left. exists 0. now nzsimpl. - intros x. split; intros [(y,H)|(y,H)]. @@ -86,7 +86,7 @@ Qed. Lemma orb_even_odd : forall n, orb (even n) (odd n) = true. Proof. - intros. + intros n. destruct (Even_or_Odd n) as [H|H]. - rewrite <- even_spec in H. now rewrite H. - rewrite <- odd_spec in H. now rewrite H, orb_true_r. @@ -94,7 +94,7 @@ Qed. Lemma negb_odd : forall n, negb (odd n) = even n. Proof. - intros. + intros n. generalize (Even_or_Odd n) (Even_Odd_False n). rewrite <- even_spec, <- odd_spec. destruct (odd n), (even n) ; simpl; intuition. @@ -188,7 +188,7 @@ Qed. Lemma even_add : forall n m, even (n+m) = Bool.eqb (even n) (even m). Proof. - intros. + intros n m. case_eq (even n); case_eq (even m); rewrite <- ?negb_true_iff, ?negb_even, ?odd_spec, ?even_spec; intros (m',Hm) (n',Hn). @@ -200,7 +200,7 @@ Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). Proof. - intros. rewrite <- !negb_even. rewrite even_add. + intros n m. rewrite <- !negb_even. rewrite even_add. now destruct (even n), (even m). Qed. @@ -208,7 +208,7 @@ Qed. Lemma even_mul : forall n m, even (mul n m) = even n || even m. Proof. - intros. + intros n m. case_eq (even n); simpl; rewrite ?even_spec. - intros (n',Hn). exists (n'*m). now rewrite Hn, mul_assoc. - case_eq (even m); simpl; rewrite ?even_spec. @@ -222,7 +222,7 @@ Qed. Lemma odd_mul : forall n m, odd (mul n m) = odd n && odd m. Proof. - intros. rewrite <- !negb_even. rewrite even_mul. + intros n m. rewrite <- !negb_even. rewrite even_mul. now destruct (even n), (even m). Qed. diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v index 01a15686e0..3b2a496229 100644 --- a/theories/Numbers/NatInt/NZPow.v +++ b/theories/Numbers/NatInt/NZPow.v @@ -238,7 +238,7 @@ Qed. Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d -> a^b <= c^d. Proof. - intros. transitivity (a^d). + intros a b c d ? ?. transitivity (a^d). - apply pow_le_mono_r; intuition order. - apply pow_le_mono_l; intuition order. Qed. diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 446ed07b53..4122632603 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -58,7 +58,7 @@ Qed. Lemma sqrt_nonneg : forall a, 0<=√a. Proof. - intros. destruct (lt_ge_cases a 0) as [Ha|Ha]. + intros a. destruct (lt_ge_cases a 0) as [Ha|Ha]. - now rewrite (sqrt_neg _ Ha). - apply sqrt_spec_nonneg. destruct (sqrt_spec a Ha). order. Qed. @@ -429,7 +429,7 @@ Qed. Lemma sqrt_up_nonneg : forall a, 0<=√°a. Proof. - intros. destruct (le_gt_cases a 0) as [Ha|Ha]. + intros a. destruct (le_gt_cases a 0) as [Ha|Ha]. - now rewrite sqrt_up_eqn0. - rewrite sqrt_up_eqn; trivial. apply le_le_succ_r, sqrt_nonneg. Qed. @@ -527,7 +527,7 @@ Lemma sqrt_sqrt_up_exact : forall a, 0<=a -> (√a == √°a <-> exists b, 0<=b /\ a == b²). Proof. intros a Ha. - split. - intros. exists √a. + split. - intros H. exists √a. split. + apply sqrt_nonneg. + generalize (sqrt_sqrt_up_spec a Ha). rewrite <-H. destruct 1; order. - intros (b & Hb & Hb'). rewrite Hb'. |