diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-26 00:57:44 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2017-06-26 10:02:10 -0400 |
| commit | 26fbc9a3fac8f2a199ff486a1db9b0ce557b3315 (patch) | |
| tree | 0e85ed72cd132ec45dcb321e4d9109570cc41ffc /src/Arithmetic/Saturated.v | |
| parent | 9ece2655d39e108a1bb91fac77c58e48708c3374 (diff) | |
Factor out admitted proof into admitted lemma
Diffstat (limited to 'src/Arithmetic/Saturated.v')
| -rw-r--r-- | src/Arithmetic/Saturated.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/Arithmetic/Saturated.v b/src/Arithmetic/Saturated.v index ddfaa8062..927369e5d 100644 --- a/src/Arithmetic/Saturated.v +++ b/src/Arithmetic/Saturated.v @@ -831,7 +831,9 @@ Section API. intros x H; apply repeat_spec in H; subst x; omega. Qed. - Axiom proof_admitted : False. + Lemma eval_pair n (p : T (S (S n))) : small p -> (snd p = 0 /\ eval (n:=S n) (fst p) = 0) <-> eval p = 0. + Admitted. + Lemma eval_nonzero n p : small p -> @nonzero n p = 0 <-> eval p = 0. Proof. destruct n as [|n]. @@ -851,7 +853,7 @@ Section API. rewrite Z.lor_eq_0_iff, IHn by (hnf in Hsmall |- *; simpl in *; eauto); clear IHn. - subst k; abstract case proof_admitted. } + exact (eval_pair n (ps, p) Hsmall). } Qed. Lemma eval_join0 n p |