diff options
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index f88ca81..9ca351a 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -671,6 +671,11 @@ Proof. destruct (zle sz 2). omegaContradiction. destruct (zle sz 4). auto. apply Zdivides_trans with 8; auto. exists 2; auto. + assert (8 <= sz -> (8 | n)). intros. + destruct (zle sz 1). omegaContradiction. + destruct (zle sz 2). omegaContradiction. + destruct (zle sz 4). omegaContradiction. + auto. destruct chunk; simpl in *; auto. apply Zone_divide. apply Zone_divide. |