1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| A.Asperti, C.Sacerdoti Coen, *)
8 (* ||A|| E.Tassi, S.Zacchiroli *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU Lesser General Public License Version 2.1 *)
13 (**************************************************************************)
16 set "baseuri" "cic:/matita/nat/minus".
18 include "nat/orders_op.ma".
19 include "nat/compare.ma".
21 let rec minus n m \def
27 | (S q) \Rightarrow minus p q ]].
30 theorem minus_n_O: \forall n:nat.eq nat n (minus n O).
31 intros.elim n.simplify.reflexivity.
35 theorem minus_n_n: \forall n:nat.eq nat O (minus n n).
36 intros.elim n.simplify.
41 theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n).
47 theorem minus_Sn_m: \forall n,m:nat.
48 le m n \to eq nat (minus (S n) m) (S (minus n m)).
51 (\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))).
52 intros.apply le_n_O_elim n1 H.
54 intros.simplify.reflexivity.
55 intros.rewrite < H.reflexivity.
56 apply le_S_S_to_le. assumption.
60 \forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m).
63 (\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)).
64 intros.apply le_n_O_elim ? H.
65 simplify.rewrite < minus_n_O.reflexivity.
66 intros.simplify.reflexivity.
67 intros.simplify.apply H.apply le_S_S_to_le.assumption.
70 theorem plus_minus_m_m: \forall n,m:nat.
71 le m n \to eq nat n (plus (minus n m) m).
73 apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)).
74 intros.apply le_n_O_elim n1 H.
76 intros.simplify.rewrite < plus_n_O.reflexivity.
77 intros.simplify.rewrite < sym_plus.simplify.
78 apply eq_f.rewrite < sym_plus.apply H.
79 apply le_S_S_to_le.assumption.
82 theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to
84 intros.apply trans_eq ? ? (plus (minus n m) m) ?.
90 theorem plus_to_minus :\forall n,m,p:nat.le m n \to
91 eq nat n (plus m p) \to eq nat (minus n m) p.
97 apply plus_minus_m_m.assumption.
100 theorem eq_minus_n_m_O: \forall n,m:nat.
101 le n m \to eq nat (minus n m) O.
103 apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
104 intros.simplify.reflexivity.
105 intros.apply False_ind.
106 (* ancora problemi con il not *)
107 apply not_le_Sn_O n1 H.
109 simplify.apply H.apply le_S_S_to_le. apply H1.
112 theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
113 intros.elim H.elim minus_Sn_n n.apply le_n.
114 rewrite > minus_Sn_m.
115 apply le_S.assumption.
116 apply lt_to_le.assumption.
120 theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
122 elim p.simplify.apply trans_le ? (plus n m) ?.
124 apply plus_le.assumption.
125 apply le_n_Sm_elim ? ? H1.
129 theorem distributive_times_minus: distributive nat times minus.
132 apply (leb_elim z y).intro.
133 cut eq nat (plus (times x (minus y z)) (times x z))
134 (plus (minus (times x y) (times x z)) (times x z)).
135 apply inj_plus_l (times x z).
137 apply trans_eq nat ? (times x y).
138 rewrite < times_plus_distr.
139 rewrite < plus_minus_m_m ? ? H.reflexivity.
140 rewrite < plus_minus_m_m ? ? ?.reflexivity.
144 rewrite > eq_minus_n_m_O.
145 rewrite > eq_minus_n_m_O (times x y).
146 rewrite < sym_times.simplify.reflexivity.
148 apply not_le_to_lt.assumption.
149 apply le_times_r.apply lt_to_le.
150 apply not_le_to_lt.assumption.
153 theorem distr_times_minus: \forall n,m,p:nat.
154 eq nat (times n (minus m p)) (minus (times n m) (times n p))
155 \def distributive_times_minus.
157 theorem le_minus_m: \forall n,m:nat. le (minus n m) n.
158 intro.elim n.simplify.apply le_n.
159 elim m.simplify.apply le_n.
160 simplify.apply le_S.apply H.