apply eq_f.assumption.
qed.
-theorem not_eq_pp_nn: \forall n,m:nat. \lnot (pp n) = (nn m).
+theorem not_eq_pp_nn: \forall n,m:nat. pp n \neq nn m.
intros.simplify. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
theorem not_eq_pp_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
-\lnot (pp n) = (cons x f).
+pp n \neq cons x f.
intros.simplify. intro.
change with match (pp n) with
[ (pp n) \Rightarrow False
theorem not_eq_nn_cons:
\forall n:nat.\forall x:Z. \forall f:fraction.
-\lnot (nn n) = (cons x f).
+nn n \neq cons x f.
intros.simplify. intro.
change with match (nn n) with
[ (pp n) \Rightarrow True
theorem eqfb_to_Prop: \forall f,g:fraction.
match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow \lnot f=g].
+|false \Rightarrow f \neq g].
intros.apply fraction_elim2
(\lambda f,g.match (eqfb f g) with
[true \Rightarrow f=g
-|false \Rightarrow \lnot f=g]).
+|false \Rightarrow f \neq g]).
intros.elim g1.
simplify.apply eqb_elim.
intro.simplify.apply eq_f.assumption.
\forall x,y:Z.
match eqZb x y with
[ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y].
+| false \Rightarrow x \neq y].
intros.
elim x.
elim y.
qed.
theorem eqZb_elim: \forall x,y:Z.\forall P:bool \to Prop.
-(x=y \to (P true)) \to (\lnot x=y \to (P false)) \to P (eqZb x y).
+(x=y \to (P true)) \to (x \neq y \to (P false)) \to P (eqZb x y).
intros.
cut
match (eqZb x y) with
[ true \Rightarrow x=y
-| false \Rightarrow \lnot x=y] \to P (eqZb x y).
+| false \Rightarrow x \neq y] \to P (eqZb x y).
apply Hcut.
apply eqZb_to_Prop.
elim (eqZb).
theorem OZ_test_to_Prop :\forall z:Z.
match OZ_test z with
[true \Rightarrow z=OZ
-|false \Rightarrow \lnot (z=OZ)].
+|false \Rightarrow z \neq OZ].
intros.elim z.
simplify.reflexivity.
simplify.intros [H].
variant inj_neg : \forall n,m:nat. neg n = neg m \to n = m
\def injective_neg.
-theorem not_eq_OZ_pos: \forall n:nat. \lnot (OZ = (pos n)).
+theorem not_eq_OZ_pos: \forall n:nat. OZ \neq pos n.
simplify.intros [n; H].
discriminate H.
qed.
-theorem not_eq_OZ_neg :\forall n:nat. \lnot (OZ = (neg n)).
+theorem not_eq_OZ_neg :\forall n:nat. OZ \neq neg n.
simplify.intros [n; H].
discriminate H.
qed.
-theorem not_eq_pos_neg :\forall n,m:nat. \lnot ((pos n) = (neg m)).
+theorem not_eq_pos_neg :\forall n,m:nat. pos n \neq neg m.
simplify.intros [n; m; H].
discriminate H.
qed.
| true : bool
| false : bool.
-theorem not_eq_true_false : \lnot true = false.
+theorem not_eq_true_false : true \neq false.
simplify.intro.
change with
match true with
theorem eqb_to_Prop: \forall n,m:nat.
match (eqb n m) with
[ true \Rightarrow n = m
-| false \Rightarrow \lnot (n = m)].
+| false \Rightarrow n \neq m].
intros.
apply nat_elim2
(\lambda n,m:nat.match (eqb n m) with
[ true \Rightarrow n = m
-| false \Rightarrow \lnot (n = m)]).
+| false \Rightarrow n \neq m]).
intro.elim n1.
simplify.reflexivity.
simplify.apply not_eq_O_S.
qed.
theorem eqb_elim : \forall n,m:nat.\forall P:bool \to Prop.
-(n=m \to (P true)) \to (\lnot n=m \to (P false)) \to (P (eqb n m)).
+(n=m \to (P true)) \to (n \neq m \to (P false)) \to (P (eqb n m)).
intros.
cut
match (eqb n m) with
[ true \Rightarrow n = m
-| false \Rightarrow \lnot (n = m)] \to (P (eqb n m)).
+| false \Rightarrow n \neq m] \to (P (eqb n m)).
apply Hcut.apply eqb_to_Prop.
elim eqb n m.
apply (H H2).
theorem leb_to_Prop: \forall n,m:nat.
match (leb n m) with
[ true \Rightarrow n \leq m
-| false \Rightarrow \lnot (n \leq m)].
+| false \Rightarrow n \nleq m].
intros.
apply nat_elim2
(\lambda n,m:nat.match (leb n m) with
[ true \Rightarrow n \leq m
-| false \Rightarrow \lnot (n \leq m)]).
+| false \Rightarrow n \nleq m]).
simplify.exact le_O_n.
simplify.exact not_le_Sn_O.
intros 2.simplify.elim (leb n1 m1).
qed.
theorem leb_elim: \forall n,m:nat. \forall P:bool \to Prop.
-(n \leq m \to (P true)) \to (\lnot (n \leq m) \to (P false)) \to
+(n \leq m \to (P true)) \to (n \nleq m \to (P false)) \to
P (leb n m).
intros.
cut
match (leb n m) with
[ true \Rightarrow n \leq m
-| false \Rightarrow \lnot (n \leq m)] \to (P (leb n m)).
+| false \Rightarrow n \nleq m] \to (P (leb n m)).
apply Hcut.apply leb_to_Prop.
elim leb n m.
apply (H H2).
\lambda n,m,q,r:nat.r < m \land n=q*m+r).
*)
-theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to \lnot m=O.
+theorem div_mod_spec_to_not_eq_O: \forall n,m,q,r.(div_mod_spec n m q r) \to m \neq O.
intros 4.simplify.intros.elim H.absurd le (S r) O.
rewrite < H1.assumption.
exact not_le_Sn_O r.
assumption.
change with nth_prime (max_prime_factor n) \divides r \to False.
intro.
-cut \lnot (mod r (nth_prime (max_prime_factor n))) = O.
+cut mod r (nth_prime (max_prime_factor n)) \neq O.
apply Hcut1.apply divides_to_mod_O.
apply lt_O_nth_prime_n.assumption.
apply plog_aux_to_not_mod_O n n ? q r.
simplify. intro.apply not_le_Sn_O O.
rewrite < H5 in \vdash (? ? %).assumption.
apply le_to_or_lt_eq.apply le_O_n.
-cut (S O) < r \lor \lnot (S O) < r.
+cut (S O) < r \lor (S O) \nlt r.
elim Hcut1.
right.
apply plog_to_lt_max_prime_factor1 n1 ? q r.
assumption.
apply le_to_or_lt_eq.apply le_O_n.assumption.
(* e adesso l'ultimo goal. TASSI: che ora non e' piu' l'ultimo :P *)
-cut (S O) < r \lor \lnot (S O) < r.
+cut (S O) < r \lor S O \nlt r.
elim Hcut2.
right.
apply plog_to_lt_max_prime_factor1 (S(S m1)) ? q r.
assumption.
qed.
(* questo va spostato in primes1.ma *)
-theorem plog_exp: \forall n,m,i. O < m \to \lnot (mod n m = O) \to
+theorem plog_exp: \forall n,m,i. O < m \to mod n m \neq O \to
\forall p. i \le p \to plog_aux p (m \sup i * n) m = pair nat nat i n.
intros 5.
elim i.
theorem plog_aux_to_Prop1: \forall p,n,m. (S O) < m \to O < n \to n \le p \to
match plog_aux p n m with
- [ (pair q r) \Rightarrow \lnot (mod r m = O)].
+ [ (pair q r) \Rightarrow mod r m \neq O].
intro.elim p.absurd O < n.assumption.
apply le_to_not_lt.assumption.
change with
[ (pair q r) \Rightarrow pair nat nat (S q) r]
| (S a) \Rightarrow pair nat nat O n1])
with
- [ (pair q r) \Rightarrow \lnot(mod r m = O)].
+ [ (pair q r) \Rightarrow mod r m \neq O].
apply nat_case1 (mod n1 m).intro.
generalize in match (H (div n1 m) m).
elim (plog_aux n (div n1 m) m).
apply trans_le ? n1.change with div n1 m < n1.
apply lt_div_n_m_n.assumption.assumption.assumption.
intros.
-change with (\lnot (mod n1 m = O)).
+change with mod n1 m \neq O.
rewrite > H4.
(* Andrea: META NOT FOUND !!!
rewrite > sym_eq. *)
qed.
theorem plog_aux_to_not_mod_O: \forall p,n,m,q,r. (S O) < m \to O < n \to n \le p \to
- pair nat nat q r = plog_aux p n m \to \lnot (mod r m = O).
+ pair nat nat q r = plog_aux p n m \to mod r m \neq O.
intros.
change with
match (pair nat nat q r) with
- [ (pair q r) \Rightarrow \lnot (mod r m = O)].
+ [ (pair q r) \Rightarrow mod r m \neq O].
rewrite > H3.
apply plog_aux_to_Prop1.
assumption.assumption.assumption.
theorem lt_times_to_lt_l:
\forall n,p,q:nat. p*(S n) < q*(S n) \to p < q.
intros.
-cut p < q \lor \lnot (p < q).
+cut p < q \lor p \nlt q.
elim Hcut.
assumption.
absurd p * (S n) < q * (S n).
theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
intros.
-cut m+p \le n \or \lnot m+p \le n.
+cut m+p \le n \or m+p \nleq n.
elim Hcut.
symmetry.apply plus_to_minus.assumption.
rewrite > assoc_plus.rewrite > sym_plus p.rewrite < plus_minus_m_m.
\def injective_S.
theorem not_eq_S : \forall n,m:nat.
-\lnot n=m \to \lnot (S n = S m).
+\lnot n=m \to S n \neq S m.
intros. simplify. intros.
apply H. apply injective_S. assumption.
qed.
[ O \Rightarrow False
| (S p) \Rightarrow True ].
-theorem not_eq_O_S : \forall n:nat. \lnot O=S n.
+theorem not_eq_O_S : \forall n:nat. O \neq S n.
intros. simplify. intros.
cut (not_zero O).
exact Hcut.
rewrite > H.exact I.
qed.
-theorem not_eq_n_Sn : \forall n:nat. \lnot n=S n.
+theorem not_eq_n_Sn : \forall n:nat. n \neq S n.
intros.elim n.
apply not_eq_O_S.
apply not_eq_S.assumption.
qed.
(* not le *)
-theorem not_le_Sn_O: \forall n:nat. \lnot (S n \leq O).
+theorem not_le_Sn_O: \forall n:nat. S n \nleq O.
intros.simplify.intros.apply leS_to_not_zero ? ? H.
qed.
-theorem not_le_Sn_n: \forall n:nat. \lnot (S n \leq n).
+theorem not_le_Sn_n: \forall n:nat. S n \nleq n.
intros.elim n.apply not_le_Sn_O.simplify.intros.cut S n1 \leq n1.
apply H.assumption.
apply le_S_S_to_le.assumption.
qed.
(* not eq *)
-theorem lt_to_not_eq : \forall n,m:nat. n<m \to \lnot (n=m).
+theorem lt_to_not_eq : \forall n,m:nat. n<m \to n \neq m.
simplify.intros.cut (le (S n) m) \to False.
apply Hcut.assumption.rewrite < H1.
apply not_le_Sn_n.
apply le_S_S_to_le.assumption.
qed.
-theorem not_le_to_lt: \forall n,m:nat. \lnot (n \leq m) \to m<n.
+theorem not_le_to_lt: \forall n,m:nat. n \nleq m \to m<n.
intros 2.
-apply nat_elim2 (\lambda n,m.\lnot (n \leq m) \to m<n).
+apply nat_elim2 (\lambda n,m.n \nleq m \to m<n).
intros.apply absurd (O \leq n1).apply le_O_n.assumption.
simplify.intros.apply le_S_S.apply le_O_n.
simplify.intros.apply le_S_S.apply H.intros.apply H1.apply le_S_S.
assumption.
qed.
-theorem lt_to_not_le: \forall n,m:nat. n<m \to \lnot (m \leq n).
+theorem lt_to_not_le: \forall n,m:nat. n<m \to m \nleq n.
simplify.intros 3.elim H.
apply not_le_Sn_n n H1.
apply H2.apply lt_to_le. apply H3.