include "nat/lt_arith.ma".
include "Z/plus.ma".
-include "higher_order_defs/functions.ma".
definition Ztimes :Z \to Z \to Z \def
\lambda x,y.
change with
eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ 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
eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(pos(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
elim y.
simplify.reflexivity.
change with
eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(neg (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ 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
eq Z (pos (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(pos (pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
change with
eq Z (neg (pred (times (S (pred (times (S n) (S n1)))) (S n2))))
(neg(pred (times (S n) (S (pred (times (S n1) (S n2))))))).
- rewrite < S_pred ? ?.rewrite < S_pred ? ?.rewrite < assoc_times.reflexivity.
+ rewrite < S_pred.rewrite < S_pred.rewrite < assoc_times.reflexivity.
apply lt_O_times_S_S.apply lt_O_times_S_S.
qed.
(minus (pred (times (S n) (S p)))
(pred (times (S n) (S q)))).
intros.
-rewrite < S_pred ? ?.
-rewrite > minus_pred_pred ? ? ? ?.
+rewrite < S_pred.
+rewrite > minus_pred_pred.
rewrite < distr_times_minus.
reflexivity.
(* we now close all positivity conditions *)
simplify.
change in match (plus p (times n (S p))) with (pred (times (S n) (S p))).
change in match (plus q (times n (S q))) with (pred (times (S n) (S q))).
-rewrite < nat_compare_pred_pred ? ? ? ?.
+rewrite < nat_compare_pred_pred.
rewrite < nat_compare_times_l.
rewrite < nat_compare_S_S.
apply nat_compare_elim p q.
variant distr_Ztimes_Zplus: \forall x,y,z.
eq Z (Ztimes x (Zplus y z)) (Zplus (Ztimes x y) (Ztimes x z)) \def
-distributive_Ztimes_Zplus.
\ No newline at end of file
+distributive_Ztimes_Zplus.