equal
deleted
inserted
replaced
576 moreover have "Elem ?y ?Z" |
576 moreover have "Elem ?y ?Z" |
577 apply (insert n_Elem_NatInterval[where q = "u - n - 1" and n=n and m=m]) |
577 apply (insert n_Elem_NatInterval[where q = "u - n - 1" and n=n and m=m]) |
578 apply (insert n_less_u) |
578 apply (insert n_less_u) |
579 apply (insert u) |
579 apply (insert u) |
580 apply auto |
580 apply auto |
581 apply arith |
|
582 done |
581 done |
583 ultimately show False by auto |
582 ultimately show False by auto |
584 qed |
583 qed |
585 moreover have "u = n \<longrightarrow> False" |
584 moreover have "u = n \<longrightarrow> False" |
586 proof |
585 proof |