diff options
| author | Hugo Herbelin | 2019-05-23 17:27:08 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-05-25 15:36:59 +0200 |
| commit | 71110a218f69a69010adde2f296e4022ef94b755 (patch) | |
| tree | db5d944a60f3d211191f10d3caa3b716af80d6ee /theories/QArith/Qcanon.v | |
| parent | 7050ceaa09a29c3f50620a8d3f8439c3d69a10d0 (diff) | |
Modifying theories to preferably use the "[= ]" syntax, and,
sometimes, to use "intros [= ...]" rather than things like "intros H;
injection H as [= ...]".
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
Diffstat (limited to 'theories/QArith/Qcanon.v')
| -rw-r--r-- | theories/QArith/Qcanon.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index f18fca99a0..9eae960086 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -43,10 +43,10 @@ Proof. generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. - injection H as <- <-. intros H (_,H'). + injection H as [= <- <-]. intros H (_,H'). destruct g as [|g|g]; [ discriminate | | now elim H ]. destruct bb as [|b|b]; simpl in *; try discriminate. - injection H' as H'. f_equal. + injection H' as [= H']. f_equal. apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l. Qed. @@ -87,7 +87,7 @@ Arguments Q2Qc q%Q. Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. Proof. split; intro H. - - now injection H as H%Qred_eq_iff. + - now injection H as [= H%Qred_eq_iff]. - apply Qc_is_canon. simpl. now rewrite H. Qed. @@ -269,7 +269,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. intros. destruct (Qmult_integral x y); try qc; auto. - injection H as H. + injection H as [= H]. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. |