diff options
| author | affeldt-aist | 2020-04-09 16:21:30 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-09 16:21:30 +0200 |
| commit | dc1ea50f04fdaada16f2a27a81ec24859b4ab843 (patch) | |
| tree | 66047a2e09d7111f8b5dfa7eb4de4ad7e61de2c3 /mathcomp/ssreflect/div.v | |
| parent | fea81ec06b1c309852c4c4062f4c5d1755c738d0 (diff) | |
| parent | 691e0c20a8934343a6840f2a19735acea6e79d05 (diff) | |
Merge pull request #473 from affeldt-aist/long_short_suffixes
switching long suffixes to short suffixes
Diffstat (limited to 'mathcomp/ssreflect/div.v')
| -rw-r--r-- | mathcomp/ssreflect/div.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v index b366055..9047a44 100644 --- a/mathcomp/ssreflect/div.v +++ b/mathcomp/ssreflect/div.v @@ -329,7 +329,7 @@ Proof. by rewrite [in RHS](divn_eq m 2) modn2 muln2 addnC half_bit_double. Qed. Lemma odd_mod m d : odd d = false -> odd (m %% d) = odd m. Proof. -by move=> d_even; rewrite [in RHS](divn_eq m d) odd_add odd_mul d_even andbF. +by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF. Qed. Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n]. |