[ O \Rightarrow GT
| (S q) \Rightarrow nat_compare p q]].
-theorem nat_compare_n_n: \forall n:nat.(eq compare (nat_compare n n) EQ).
+theorem nat_compare_n_n: \forall n:nat. nat_compare n n = EQ.
intro.elim n.
simplify.reflexivity.
simplify.assumption.
qed.
theorem nat_compare_S_S: \forall n,m:nat.
-eq compare (nat_compare n m) (nat_compare (S n) (S m)).
+nat_compare n m = nat_compare (S n) (S m).
intros.simplify.reflexivity.
qed.
theorem nat_compare_to_Prop: \forall n,m:nat.
match (nat_compare n m) with
[ LT \Rightarrow (lt n m)
- | EQ \Rightarrow (eq nat n m)
+ | EQ \Rightarrow n=m
| GT \Rightarrow (lt m n) ].
intros.
apply nat_elim2 (\lambda n,m.match (nat_compare n m) with
[ LT \Rightarrow (lt n m)
- | EQ \Rightarrow (eq nat n m)
+ | EQ \Rightarrow n=m
| GT \Rightarrow (lt m n) ]).
intro.elim n1.simplify.reflexivity.
simplify.apply le_S_S.apply le_O_n.
qed.
theorem nat_compare_n_m_m_n: \forall n,m:nat.
-eq compare (nat_compare n m) (compare_invert (nat_compare m n)).
+nat_compare n m = compare_invert (nat_compare m n).
intros.
-apply nat_elim2 (\lambda n,m.eq compare (nat_compare n m) (compare_invert (nat_compare m n))).
+apply nat_elim2 (\lambda n,m. nat_compare n m = compare_invert (nat_compare m n)).
intros.elim n1.simplify.reflexivity.
simplify.reflexivity.
intro.elim n1.simplify.reflexivity.
qed.
theorem nat_compare_elim : \forall n,m:nat. \forall P:compare \to Prop.
-((lt n m) \to (P LT)) \to ((eq nat n m) \to (P EQ)) \to ((lt m n) \to (P GT)) \to
+((lt n m) \to (P LT)) \to (n=m \to (P EQ)) \to ((lt m n) \to (P GT)) \to
(P (nat_compare n m)).
intros.
cut match (nat_compare n m) with
[ LT \Rightarrow (lt n m)
-| EQ \Rightarrow (eq nat n m)
+| EQ \Rightarrow n=m
| GT \Rightarrow (lt m n)] \to
(P (nat_compare n m)).
apply Hcut.apply nat_compare_to_Prop.