diff options
| author | Théo Zimmermann | 2019-05-25 18:05:29 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-25 18:05:29 +0200 |
| commit | 9241a6e25ff132a27762963b06ae1095c783c25f (patch) | |
| tree | db5d944a60f3d211191f10d3caa3b716af80d6ee /theories/Numbers/Cyclic/ZModulo/ZModulo.v | |
| parent | 5727443376480be4793757fd5507621ad4f09509 (diff) | |
| parent | 71110a218f69a69010adde2f296e4022ef94b755 (diff) | |
Merge PR #9288: Giving preference to syntax "injection ... as [= pat1 ... patn]".
Reviewed-by: Zimmi48
Diffstat (limited to 'theories/Numbers/Cyclic/ZModulo/ZModulo.v')
| -rw-r--r-- | theories/Numbers/Cyclic/ZModulo/ZModulo.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 4bcd22543f..94da55b3f3 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -372,7 +372,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H as ? ?. + destruct 1; injection H as [= ? ?]. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -414,7 +414,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1 as ? ?. + injection H1 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -525,7 +525,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4 as ? ?. + injection H4 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. |