changeset 62390 | 842917225d56 |
parent 46912 | e0cd5c4df8e6 |
child 63146 | f1ecba0272f9 |
62380:29800666e526 | 62390:842917225d56 |
---|---|
334 done |
334 done |
335 |
335 |
336 |
336 |
337 (** Towards lift_4 ***) |
337 (** Towards lift_4 ***) |
338 |
338 |
339 declare split_if_asm [split] |
339 declare if_split_asm [split] |
340 |
340 |
341 |
341 |
342 (*lem_lift_4_1 *) |
342 (*lem_lift_4_1 *) |
343 lemma E_thm12a: |
343 lemma E_thm12a: |
344 "0 < N ==> |
344 "0 < N ==> |