equal
deleted
inserted
replaced
4 |
4 |
5 declare div_mult_self_is_m [simp del] |
5 declare div_mult_self_is_m [simp del] |
6 |
6 |
7 lemma div_mult_self_is_m: |
7 lemma div_mult_self_is_m: |
8 "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
8 "0<n \<Longrightarrow> (m*n) div n = (m::nat)" |
9 apply (insert mod_div_equality [of "m*n" n]) |
9 apply (insert div_mult_mod_eq [of "m*n" n]) |
10 apply simp |
10 apply simp |
11 done |
11 done |
12 |
12 |
13 |
13 |
14 lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)" |
14 lemma "(\<forall>x. P x) \<and> (\<exists>x. Q x) \<longrightarrow> (\<forall>x. P x \<and> Q x)" |