diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-21 17:29:45 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-21 17:29:45 -0700 |
| commit | bb98cc66439c58ede6e98d0188ce8299a5c382f5 (patch) | |
| tree | 8cdfa7419a2e869a3324bda8015963a31aaea830 /src/Experiments | |
| parent | 87452544650128a0138737ab118ab31f5815eb9f (diff) | |
NPeano.modulo became Nat.modulo in 8.5
Diffstat (limited to 'src/Experiments')
| -rw-r--r-- | src/Experiments/DerivationsOptionRectLetInEncoding.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/Experiments/DerivationsOptionRectLetInEncoding.v b/src/Experiments/DerivationsOptionRectLetInEncoding.v index 4787ad0b1..d03bafbb1 100644 --- a/src/Experiments/DerivationsOptionRectLetInEncoding.v +++ b/src/Experiments/DerivationsOptionRectLetInEncoding.v @@ -229,7 +229,9 @@ Proof. induction n; auto. Qed. Lemma Z_of_nat_nonzero : forall m, m <> 0 -> (0 < Z.of_nat m)%Z. Proof. intros. destruct m; [congruence|reflexivity]. Qed. -Local Infix "mod" := NPeano.modulo : nat_scope. +Section with_unqualified_modulo. +Import NPeano Nat. +Local Infix "mod" := modulo : nat_scope. Lemma N_of_nat_modulo : forall n m, m <> 0 -> N.of_nat (n mod m)%nat = (N.of_nat n mod N.of_nat m)%N. Proof. intros. @@ -242,6 +244,7 @@ Proof. rewrite Znat.Z2N.inj_mod by (auto using Znat.Nat2Z.is_nonneg, Z_of_nat_nonzero). rewrite !Z_to_N_Z_of_nat, !Znat.N2Z.id; reflexivity. Qed. +End with_unqualified_modulo. Lemma encoding_canonical' {T} {B} {encoding:canonical encoding of T as B} : forall a b, enc a = enc b -> a = b. |