equal
deleted
inserted
replaced
528 definition |
528 definition |
529 pred_nat :: "(nat * nat) set" where |
529 pred_nat :: "(nat * nat) set" where |
530 "pred_nat = {(m, n). n = Suc m}" |
530 "pred_nat = {(m, n). n = Suc m}" |
531 |
531 |
532 definition |
532 definition |
533 less_than :: "(nat * nat)set" where |
533 less_than :: "(nat * nat) set" where |
534 "less_than = pred_nat^+" |
534 "less_than = pred_nat^+" |
535 |
535 |
536 lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n" |
536 lemma less_eq: "(m, n) \<in> pred_nat^+ \<longleftrightarrow> m < n" |
537 unfolding less_nat_rel pred_nat_def trancl_def by simp |
537 unfolding less_nat_rel pred_nat_def trancl_def by simp |
538 |
538 |