simplify.exact I.
elim y. simplify.exact I.
simplify.
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
- per via delle coercions! *)
cut match (nat_compare n1 n) with
[ LT \Rightarrow n1<n
| EQ \Rightarrow n1=n
| GT \Rightarrow n<n1] \to
match (nat_compare n1 n) with
-[ LT \Rightarrow (le (S n1) n)
+[ LT \Rightarrow (S n1) \leq n
| EQ \Rightarrow neg n = neg n1
-| GT \Rightarrow (le (S n) n1)].
+| GT \Rightarrow (S n) \leq n1].
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n1 n).
simplify.exact H.
elim y.simplify.exact I.
simplify.exact I.
simplify.
-(*CSC: qui uso le perche' altrimenti ci sono troppe scelte
- per via delle coercions! *)
cut match (nat_compare n n1) with
[ LT \Rightarrow n<n1
| EQ \Rightarrow n=n1
| GT \Rightarrow n1<n] \to
match (nat_compare n n1) with
-[ LT \Rightarrow (le (S n) n1)
+[ LT \Rightarrow (S n) \leq n1
| EQ \Rightarrow pos n = pos n1
-| GT \Rightarrow (le (S n1) n)].
+| GT \Rightarrow (S n1) \leq n].
apply Hcut. apply nat_compare_to_Prop.
elim (nat_compare n n1).
simplify.exact H.