simplify.reflexivity.
qed.
theorem symmetric_Ztimes : symmetric Z Ztimes.
-change with \forall x,y:Z. x*y = y*x.
+change with (\forall x,y:Z. x*y = y*x).
intros.elim x.rewrite > Ztimes_z_OZ.reflexivity.
elim y.simplify.reflexivity.
-change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
-change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
elim y.simplify.reflexivity.
-change with neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n))).
+change with (neg (pred ((S n) * (S n1))) = neg (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
-change with pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n))).
+change with (pos (pred ((S n) * (S n1))) = pos (pred ((S n1) * (S n)))).
rewrite < sym_times.reflexivity.
qed.
\def symmetric_Ztimes.
theorem associative_Ztimes: associative Z Ztimes.
-change with \forall x,y,z:Z. (x*y)*z = x*(y*z).
+change with (\forall x,y,z:Z. (x*y)*z = x*(y*z)).
intros.elim x.
simplify.reflexivity.
elim y.
elim z.
simplify.reflexivity.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim z.
simplify.reflexivity.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim y.
elim z.
simplify.reflexivity.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim z.
simplify.reflexivity.
change with
- pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- pos (pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (pos (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ pos (pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
- neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
- neg(pred ((S n) * (S (pred ((S n1) * (S n2)))))).
+ (neg (pred ((S (pred ((S n) * (S n1)))) * (S n2))) =
+ neg(pred ((S n) * (S (pred ((S n1) * (S n2))))))).
rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
(* we now close all positivity conditions *)
apply lt_O_times_S_S.
apply lt_O_times_S_S.
-simplify.
+simplify.unfold lt.
apply le_SO_minus. exact H.
qed.
(pos n)*((neg p)+(pos q)) = (pos n)*(neg p)+ (pos n)*(pos q).
intros.
simplify.
-change in match p + n * (S p) with pred ((S n) * (S p)).
-change in match q + n * (S q) with pred ((S n) * (S q)).
+change in match (p + n * (S p)) with (pred ((S n) * (S p))).
+change in match (q + n * (S q)) with (pred ((S n) * (S q))).
rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.
-apply nat_compare_elim p q.
+apply (nat_compare_elim p q).
intro.
(* uff *)
-change with pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
- pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p))))).
-rewrite < times_minus1 n q p H.reflexivity.
+change with (pos (pred ((S n) * (S (pred ((S q) - (S p)))))) =
+ pos (pred ((pred ((S n) * (S q))) - (pred ((S n) * (S p)))))).
+rewrite < (times_minus1 n q p H).reflexivity.
intro.rewrite < H.simplify.reflexivity.
intro.
-change with neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
- neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q))))).
-rewrite < times_minus1 n p q H.reflexivity.
+change with (neg (pred ((S n) * (S (pred ((S p) - (S q)))))) =
+ neg (pred ((pred ((S n) * (S p))) - (pred ((S n) * (S q)))))).
+rewrite < (times_minus1 n p q H).reflexivity.
(* two more positivity conditions from nat_compare_pred_pred *)
apply lt_O_times_S_S.
apply lt_O_times_S_S.
lemma distributive2_Ztimes_pos_Zplus:
distributive2 nat Z (\lambda n,z. (pos n) * z) Zplus.
-change with \forall n,y,z.
-(pos n) * (y + z) = (pos n) * y + (pos n) * z.
+change with (\forall n,y,z.
+(pos n) * (y + z) = (pos n) * y + (pos n) * z).
intros.elim y.
reflexivity.
elim z.
reflexivity.
change with
- pos (pred ((S n) * ((S n1) + (S n2)))) =
- pos (pred ((S n) * (S n1) + (S n) * (S n2))).
+ (pos (pred ((S n) * ((S n1) + (S n2)))) =
+ pos (pred ((S n) * (S n1) + (S n) * (S n2)))).
rewrite < distr_times_plus.reflexivity.
apply Ztimes_Zplus_pos_pos_neg.
elim z.
reflexivity.
apply Ztimes_Zplus_pos_neg_pos.
change with
- neg (pred ((S n) * ((S n1) + (S n2)))) =
- neg (pred ((S n) * (S n1) + (S n) * (S n2))).
+ (neg (pred ((S n) * ((S n1) + (S n2)))) =
+ neg (pred ((S n) * (S n1) + (S n) * (S n2)))).
rewrite < distr_times_plus.reflexivity.
qed.
lemma distributive2_Ztimes_neg_Zplus :
distributive2 nat Z (\lambda n,z. (neg n) * z) Zplus.
-change with \forall n,y,z.
-(neg n) * (y + z) = (neg n) * y + (neg n) * z.
+change with (\forall n,y,z.
+(neg n) * (y + z) = (neg n) * y + (neg n) * z).
intros.
rewrite > Ztimes_neg_Zopp.
rewrite > distr_Ztimes_Zplus_pos.
distributive2_Ztimes_neg_Zplus.
theorem distributive_Ztimes_Zplus: distributive Z Ztimes Zplus.
-change with \forall x,y,z:Z. x * (y + z) = x*y + x*z.
+change with (\forall x,y,z:Z. x * (y + z) = x*y + x*z).
intros.elim x.
(* case x = OZ *)
simplify.reflexivity.