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 (**************************************************************************)
15 set "baseuri" "cic:/matita/nat/minus.ma".
17 include "nat/orders_op.ma".
18 include "nat/times.ma".
20 let rec minus n m \def
26 | (S q) \Rightarrow minus p q ]].
29 theorem minus_n_O: \forall n:nat.eq nat n (minus n O).
30 intros.elim n.simplify.reflexivity.
34 theorem minus_n_n: \forall n:nat.eq nat O (minus n n).
35 intros.elim n.simplify.
40 theorem minus_Sn_n: \forall n:nat.eq nat (S O) (minus (S n) n).
46 theorem minus_Sn_m: \forall n,m:nat.
47 le m n \to eq nat (minus (S n) m) (S (minus n m)).
50 (\lambda n,m.le m n \to eq nat (minus (S n) m) (S (minus n m))).
51 intros.apply le_n_O_elim n1 H.
53 intros.simplify.reflexivity.
54 intros.rewrite < H.reflexivity.
55 apply le_S_S_to_le. assumption.
59 \forall n,m,p:nat. le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m).
62 (\lambda n,m.\forall p:nat.le m n \to eq nat (plus (minus n m) p) (minus (plus n p) m)).
63 intros.apply le_n_O_elim ? H.
64 simplify.rewrite < minus_n_O.reflexivity.
65 intros.simplify.reflexivity.
66 intros.simplify.apply H.apply le_S_S_to_le.assumption.
69 theorem plus_minus_m_m: \forall n,m:nat.
70 le m n \to eq nat n (plus (minus n m) m).
72 apply nat_elim2 (\lambda n,m.le m n \to eq nat n (plus (minus n m) m)).
73 intros.apply le_n_O_elim n1 H.
75 intros.simplify.rewrite < plus_n_O.reflexivity.
76 intros.simplify.rewrite < sym_plus.simplify.
77 apply eq_f.rewrite < sym_plus.apply H.
78 apply le_S_S_to_le.assumption.
81 theorem minus_to_plus :\forall n,m,p:nat.le m n \to eq nat (minus n m) p \to
83 intros.apply trans_eq ? ? (plus (minus n m) m) ?.
89 theorem plus_to_minus :\forall n,m,p:nat.le m n \to
90 eq nat n (plus m p) \to eq nat (minus n m) p.
96 apply plus_minus_m_m.assumption.
99 theorem minus_ge_O: \forall n,m:nat.
100 le n m \to eq nat (minus n m) O.
102 apply nat_elim2 (\lambda n,m.le n m \to eq nat (minus n m) O).
103 intros.simplify.reflexivity.
104 intros.apply False_ind.
105 (* ancora problemi con il not *)
106 apply not_le_Sn_O n1 H.
108 simplify.apply H.apply le_S_S_to_le. apply H1.
111 theorem le_SO_minus: \forall n,m:nat.le (S n) m \to le (S O) (minus m n).
112 intros.elim H.elim minus_Sn_n n.apply le_n.
113 rewrite > minus_Sn_m.
114 apply le_S.assumption.
115 apply lt_to_le.assumption.
119 theorem le_plus_minus: \forall n,m,p. (le (plus n m) p) \to (le n (minus p m)).
121 elim p.simplify.apply trans_le ? (plus n m) ?.
123 apply plus_le.assumption.
124 apply le_n_Sm_elim ? ? H1.
129 theorem times_minus_distr: \forall n,m,p:nat.
130 eq nat (times n (minus m p)) (minus (times n m) (times n p)).
132 apply (leb_ind p m).intro.
133 cut eq nat (plus (times n (minus m p)) (times n p)) (plus (minus (times n m) (times n p)) (times n p)).
134 apply plus_injective_right ? ? (times n p).
136 apply trans_eq nat ? (times n m).
137 elim (times_plus_distr ? ? ?).
138 elim (minus_plus ? ? H).apply refl_equal.
139 elim (minus_plus ? ? ?).apply refl_equal.
140 apply times_le_monotony_left.
143 elim sym_eq ? ? ? (minus_ge_O ? ? ?).
144 elim sym_eq ? ? ? (minus_ge_O ? ? ?).
145 elim (sym_times ? ?).simplify.apply refl_equal.
147 apply times_le_monotony_left.
148 cut (lt m p) \to (le m p).
149 apply Hcut.simplify.apply not_le_lt ? ? H.
150 intro.apply lt_le.apply H1.
151 cut (lt m p) \to (le m p).
152 apply Hcut.simplify.apply not_le_lt ? ? H.
153 intro.apply lt_le.apply H1.
156 theorem minus_le: \forall n,m:nat. le (minus n m) n.
157 intro.elim n.simplify.apply le_n.
158 elim m.simplify.apply le_n.
159 simplify.apply le_S.apply H.