| cmp_gt : m < n → cmp_cases n m.
lemma cmp_nat: ∀n,m.cmp_cases n m.
intros; generalize in match (nat_compare_to_Prop n m);
cases (nat_compare n m); intros;
| cmp_gt : m < n → cmp_cases n m.
lemma cmp_nat: ∀n,m.cmp_cases n m.
intros; generalize in match (nat_compare_to_Prop n m);
cases (nat_compare n m); intros;