[ LT \Rightarrow n<n1
| EQ \Rightarrow n=n1
| GT \Rightarrow n1<n] \to
match (nat_compare n n1) with
[ LT \Rightarrow (S n) \leq n1
| EQ \Rightarrow pos n = pos n1
[ LT \Rightarrow n<n1
| EQ \Rightarrow n=n1
| GT \Rightarrow n1<n] \to
match (nat_compare n n1) with
[ LT \Rightarrow (S n) \leq n1
| EQ \Rightarrow pos n = pos n1