Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(*                      Evgeny Makarov, INRIA, 2007                     *)
(************************************************************************)

Require Export ZAdd.

Module ZMulProp (Import Z : ZAxiomsMiniSig').
Include ZAddProp Z.
A note on naming: right (correspondingly, left) distributivity happens when the sum is multiplied by a number on the right (left), not when the sum itself is the right (left) factor in the product (see planetmath.org and mathworld.wolfram.com). In the old library BinInt, distributivity over subtraction was named correctly, but distributivity over addition was named incorrectly. The names in Isabelle/HOL library are also incorrect.
Theorems that are either not valid on N or have different proofs on N and Z 
forall n m : t, n * P m == n * m - n


forall n m : t, n * P m == n * m - n


n, m:t
n * P m == n * m - n


n, m:t
n * P m == n * S (P m) - n

now rewrite mul_succ_r, <- add_sub_assoc, sub_diag, add_0_r.
Qed.


forall n m : t, P n * m == n * m - m


forall n m : t, P n * m == n * m - m


n, m:t
m * P n == m * n - m
 apply mul_pred_r.
Qed.


forall n m : t, - n * m == - (n * m)


forall n m : t, - n * m == - (n * m)


n, m:t
- n * m == - (n * m)
 
n, m:t
- n * m + n * m == 0

now rewrite <- mul_add_distr_r, add_opp_diag_l, mul_0_l.
Qed.


forall n m : t, n * - m == - (n * m)


forall n m : t, n * - m == - (n * m)

intros n m; rewrite (mul_comm n (- m)), (mul_comm n m); apply mul_opp_l.
Qed.


forall n m : t, - n * - m == n * m


forall n m : t, - n * - m == n * m

intros n m; now rewrite mul_opp_l, mul_opp_r, opp_involutive.
Qed.


forall n m : t, - n * m == n * - m


forall n m : t, - n * m == n * - m


n, m:t
- n * m == n * - m
 now rewrite mul_opp_l, <- mul_opp_r.
Qed.


forall n m p : t, n * (m - p) == n * m - n * p


forall n m p : t, n * (m - p) == n * m - n * p


n, m, p:t
n * (m - p) == n * m - n * p
 
n, m, p:t
n * (m + - p) == n * m + - (n * p)
 
n, m, p:t
n * m + n * - p == n * m + - (n * p)

now rewrite mul_opp_r.
Qed.


forall n m p : t, (n - m) * p == n * p - m * p


forall n m p : t, (n - m) * p == n * p - m * p

intros n m p; rewrite (mul_comm (n - m) p), (mul_comm n p), (mul_comm m p);
now apply mul_sub_distr_l.
Qed.

End ZMulProp.