diff options
| author |  Jason Gross <jagro@google.com> | 2018-07-17 18:53:26 -0400 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2018-07-17 18:53:26 -0400 |
| commit | 74353376d2a9f69991300e6a0704f85bc642b1c4 (patch) | |
| tree | ec84e1e32b547de102ad5ff781ad91ff3dbfd513 /src | |
| parent | 10d1d4825c00d432b76420bb24f1b9df732ec4b3 (diff) | |
Remove a lemma that's been moved to NatUtil
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Arithmetic.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v index 013b28b93..cb49424ab 100644 --- a/src/Experiments/NewPipeline/Arithmetic.v +++ b/src/Experiments/NewPipeline/Arithmetic.v @@ -1690,13 +1690,6 @@ Module Rows. rewrite Columns.length_from_associational in *; auto. Qed. - (* TODO : move *) - Lemma max_0_iff a b : Nat.max a b = 0%nat <-> (a = 0%nat /\ b = 0%nat). - Proof. - destruct a, b; try tauto. - rewrite <-Nat.succ_max_distr. - split; [ | destruct 1]; congruence. - Qed. Lemma max_column_size_zero_iff x : max_column_size x = 0%nat <-> (forall c, In c x -> c = nil). Proof. |