[O \Rightarrow (S p)
| (S q) \Rightarrow minus p q ]].
+interpretation "natural minus" 'minus x y = (cic:/matita/nat/minus/minus.con x y).
-theorem minus_n_O: \forall n:nat.n=minus n O.
+theorem minus_n_O: \forall n:nat.n=n-O.
intros.elim n.simplify.reflexivity.
simplify.reflexivity.
qed.
-theorem minus_n_n: \forall n:nat.O=minus n n.
+theorem minus_n_n: \forall n:nat.O=n-n.
intros.elim n.simplify.
reflexivity.
simplify.apply H.
qed.
-theorem minus_Sn_n: \forall n:nat. S O = minus (S n) n.
+theorem minus_Sn_n: \forall n:nat. S O = (S n)-n.
intro.elim n.
simplify.reflexivity.
elim H.reflexivity.
qed.
-theorem minus_Sn_m: \forall n,m:nat.
-le m n \to minus (S n) m = S (minus n m).
+theorem minus_Sn_m: \forall n,m:nat. m \leq n \to (S n)-m = S (n-m).
intros 2.
apply nat_elim2
-(\lambda n,m.le m n \to minus (S n) m = S (minus n m)).
+(\lambda n,m.m \leq n \to (S n)-m = S (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 plus (minus n m) p = minus (plus n p) m.
+\forall n,m,p:nat. m \leq n \to (n-m)+p = (n+p)-m.
intros 2.
apply nat_elim2
-(\lambda n,m.\forall p:nat.le m n \to plus (minus n m) p = minus (plus n p) m).
+(\lambda n,m.\forall p:nat.m \leq n \to (n-m)+p = (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 n = plus (minus n m) m.
+m \leq n \to n = (n-m)+m.
intros 2.
-apply nat_elim2 (\lambda n,m.le m n \to n = plus (minus n m) m).
+apply nat_elim2 (\lambda n,m.m \leq n \to n = (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 minus n m = p \to
-n = plus m p.
-intros.apply trans_eq ? ? (plus (minus n m) m) ?.
+theorem minus_to_plus :\forall n,m,p:nat.m \leq n \to n-m = p \to
+n = m+p.
+intros.apply trans_eq ? ? ((n-m)+m) ?.
apply plus_minus_m_m.
apply H.elim H1.
apply sym_plus.
qed.
-theorem plus_to_minus :\forall n,m,p:nat.le m n \to
-n = plus m p \to minus n m = p.
+theorem plus_to_minus :\forall n,m,p:nat.m \leq n \to
+n = m+p \to 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 minus n m = O.
+n \leq m \to n-m = O.
intros 2.
-apply nat_elim2 (\lambda n,m.le n m \to minus n m = O).
+apply nat_elim2 (\lambda n,m.n \leq m \to n-m = O).
intros.simplify.reflexivity.
intros.apply False_ind.
(* ancora problemi con il not *)
simplify.apply H.apply le_S_S_to_le. apply H1.
qed.
-theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
+theorem le_SO_minus: \forall n,m:nat.S n \leq m \to S O \leq m-n.
intros.elim H.elim minus_Sn_n n.apply le_n.
rewrite > minus_Sn_m.
apply le_S.assumption.
qed.
(*
-theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
+theorem le_plus_minus: \forall n,m,p. n+m \leq p \to n \leq p-m.
intros 3.
-elim p.simplify.apply trans_le ? (plus n m) ?.
+elim p.simplify.apply trans_le ? (n+m) ?.
elim sym_plus ? ?.
apply plus_le.assumption.
apply le_n_Sm_elim ? ? H1.
simplify.
intros.
apply (leb_elim z y).intro.
-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).
+cut x*(y-z)+x*z = (x*y-x*z)+x*z.
+apply inj_plus_l (x*z).
assumption.
-apply trans_eq nat ? (times x y).
+apply trans_eq nat ? (x*y).
rewrite < times_plus_distr.
rewrite < plus_minus_m_m ? ? H.reflexivity.
rewrite < plus_minus_m_m ? ? ?.reflexivity.
assumption.
intro.
rewrite > eq_minus_n_m_O.
-rewrite > eq_minus_n_m_O (times x y).
+rewrite > eq_minus_n_m_O (x*y).
rewrite < sym_times.simplify.reflexivity.
apply lt_to_le.
apply not_le_to_lt.assumption.
apply not_le_to_lt.assumption.
qed.
-theorem distr_times_minus: \forall n,m,p:nat.
-times n (minus m p) = minus (times n m) (times n p)
+theorem distr_times_minus: \forall n,m,p:nat. n*(m-p) = n*m-n*p
\def distributive_times_minus.
-theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
+theorem le_minus_m: \forall n,m:nat. n-m \leq n.
intro.elim n.simplify.apply le_n.
elim m.simplify.apply le_n.
simplify.apply le_S.apply H.