| (S q) \Rightarrow minus p q ]].
-theorem minus_n_O: \forall n:nat.eq nat n (minus n O).
+theorem minus_n_O: \forall n:nat.n=minus n O.
intros.elim n.simplify.reflexivity.
simplify.reflexivity.
qed.
-theorem minus_n_n: \forall n:nat.eq nat O (minus n n).
+theorem minus_n_n: \forall n:nat.O=minus n n.
intros.elim n.simplify.
reflexivity.
simplify.apply H.
qed.
-theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n).
+theorem minus_Sn_n: \forall n:nat. S O = minus (S n) n.
intro.elim n.
simplify.reflexivity.
elim H.reflexivity.
qed.
theorem minus_Sn_m: \forall n,m:nat.
-le m n \to eq nat (minus (S n) m) (S (minus n m)).
+le m n \to minus (S n) m = S (minus n m).
intros 2.
apply nat_elim2
-(\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))).
+(\lambda n,m.le m n \to minus (S n) m = S (minus n m)).
intros.apply le_n_O_elim n1 H.
simplify.reflexivity.
intros.simplify.reflexivity.
qed.
theorem plus_minus:
-\forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m).
+\forall n,m,p:nat. le m n \to plus (minus n m) p = minus (plus n p) m.
intros 2.
apply nat_elim2
-(\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)).
+(\lambda n,m.\forall p:nat.le m n \to plus (minus n m) p = minus (plus n p) m).
intros.apply le_n_O_elim ? H.
simplify.rewrite < minus_n_O.reflexivity.
intros.simplify.reflexivity.
qed.
theorem plus_minus_m_m: \forall n,m:nat.
-le m n \to eq nat n (plus (minus n m) m).
+le m n \to n = plus (minus n m) m.
intros 2.
-apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)).
+apply nat_elim2 (\lambda n,m.le m n \to n = plus (minus n m) m).
intros.apply le_n_O_elim n1 H.
reflexivity.
intros.simplify.rewrite < plus_n_O.reflexivity.
apply le_S_S_to_le.assumption.
qed.
-theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to
-eq nat n (plus m p).
+theorem minus_to_plus :\forall n,m,p:nat.le m n \to minus n m = p \to
+n = plus m p.
intros.apply trans_eq ? ? (plus (minus n m) m) ?.
apply plus_minus_m_m.
apply H.elim H1.
qed.
theorem plus_to_minus :\forall n,m,p:nat.le m n \to
-eq nat n (plus m p) \to eq nat (minus n m) p.
+n = plus m p \to minus n m = p.
intros.
apply inj_plus_r m.
rewrite < H1.
qed.
theorem eq_minus_n_m_O: \forall n,m:nat.
-le n m \to eq nat (minus n m) O.
+le n m \to minus n m = O.
intros 2.
-apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
+apply nat_elim2 (\lambda n,m.le n m \to minus n m = O).
intros.simplify.reflexivity.
intros.apply False_ind.
(* ancora problemi con il not *)
simplify.
intros.
apply (leb_elim z y).intro.
-cut eq nat (plus (times x (minus y z)) (times x z))
- (plus (minus (times x y) (times x z)) (times x z)).
+cut plus (times x (minus y z)) (times x z) =
+ plus (minus (times x y) (times x z)) (times x z).
apply inj_plus_l (times x z).
assumption.
apply trans_eq nat ? (times x y).
qed.
theorem distr_times_minus: \forall n,m,p:nat.
-eq nat (times n (minus m p)) (minus (times n m) (times n p))
+times n (minus m p) = minus (times n m) (times n p)
\def distributive_times_minus.
theorem le_minus_m: \forall n,m:nat. le (minus n m) n.