# Library Coq.Arith.Mult

``` Require Export Plus. Require Export Minus. Require Export Lt. Require Export Le. Open Local Scope nat_scope. Implicit Types m n p : nat. ```
Zero property
``` Lemma mult_0_r : forall n, n * 0 = 0. Proof. intro; symmetry in |- *; apply mult_n_O. Qed. Lemma mult_0_l : forall n, 0 * n = 0. Proof. reflexivity. Qed. ```
Distributivity
``` Lemma mult_plus_distr_r : forall n m p, (n + m) * p = n * p + m * p. Proof. intros; elim n; simpl in |- *; intros; auto with arith. elim plus_assoc; elim H; auto with arith. Qed. Hint Resolve mult_plus_distr_r: arith v62. Lemma mult_plus_distr_l : forall n m p, n * (m + p) = n * m + n * p. Proof.   induction n. trivial.   intros. simpl in |- *. rewrite (IHn m p). apply sym_eq. apply plus_permute_2_in_4. Qed. Lemma mult_minus_distr_r : forall n m p, (n - m) * p = n * p - m * p. Proof. intros; pattern n, m in |- *; apply nat_double_ind; simpl in |- *; intros;  auto with arith. elim minus_plus_simpl_l_reverse; auto with arith. Qed. Hint Resolve mult_minus_distr_r: arith v62. ```
Associativity
``` Lemma mult_assoc_reverse : forall n m p, n * m * p = n * (m * p). Proof. intros; elim n; intros; simpl in |- *; auto with arith. rewrite mult_plus_distr_r. elim H; auto with arith. Qed. Hint Resolve mult_assoc_reverse: arith v62. Lemma mult_assoc : forall n m p, n * (m * p) = n * m * p. Proof. auto with arith. Qed. Hint Resolve mult_assoc: arith v62. ```
Commutativity
``` Lemma mult_comm : forall n m, n * m = m * n. Proof. intros; elim n; intros; simpl in |- *; auto with arith. elim mult_n_Sm. elim H; apply plus_comm. Qed. Hint Resolve mult_comm: arith v62. ```
1 is neutral
``` Lemma mult_1_l : forall n, 1 * n = n. Proof. simpl in |- *; auto with arith. Qed. Hint Resolve mult_1_l: arith v62. Lemma mult_1_r : forall n, n * 1 = n. Proof. intro; elim mult_comm; auto with arith. Qed. Hint Resolve mult_1_r: arith v62. ```
Compatibility with orders
``` Lemma mult_O_le : forall n m, m = 0 \/ n <= m * n. Proof. induction m; simpl in |- *; auto with arith. Qed. Hint Resolve mult_O_le: arith v62. Lemma mult_le_compat_l : forall n m p, n <= m -> p * n <= p * m. Proof.   induction p as [| p IHp]. intros. simpl in |- *. apply le_n.   intros. simpl in |- *. apply plus_le_compat. assumption.   apply IHp. assumption. Qed. Hint Resolve mult_le_compat_l: arith. Lemma mult_le_compat_r : forall n m p, n <= m -> n * p <= m * p. intros m n p H. rewrite mult_comm. rewrite (mult_comm n). auto with arith. Qed. Lemma mult_le_compat :  forall n m p (q:nat), n <= m -> p <= q -> n * p <= m * q. Proof. intros m n p q Hmn Hpq; induction Hmn. induction Hpq. apply le_n. rewrite <- mult_n_Sm; apply le_trans with (m * m0). assumption. apply le_plus_l. simpl in |- *; apply le_trans with (m0 * q). assumption. apply le_plus_r. Qed. Lemma mult_S_lt_compat_l : forall n m p, m < p -> S n * m < S n * p. Proof.   intro m; induction m. intros. simpl in |- *. rewrite <- plus_n_O. rewrite <- plus_n_O. assumption.   intros. exact (plus_lt_compat _ _ _ _ H (IHm _ _ H)). Qed. Hint Resolve mult_S_lt_compat_l: arith. Lemma mult_lt_compat_r : forall n m p, n < m -> 0 < p -> n * p < m * p. intros m n p H H0. induction p. elim (lt_irrefl _ H0). rewrite mult_comm. replace (n * S p) with (S p * n); auto with arith. Qed. Lemma mult_S_le_reg_l : forall n m p, S n * m <= S n * p -> m <= p. Proof.   intros m n p H. elim (le_or_lt n p). trivial.   intro H0. cut (S m * n < S m * n). intro. elim (lt_irrefl _ H1).   apply le_lt_trans with (m := S m * p). assumption.   apply mult_S_lt_compat_l. assumption. Qed. ```
n|->2*n and n|->2n+1 have disjoint image
``` Theorem odd_even_lem : forall p q, 2 * p + 1 <> 2 * q. intros p; elim p; auto. intros q; case q; simpl in |- *. red in |- *; intros; discriminate. intros q'; rewrite (fun x y => plus_comm x (S y)); simpl in |- *; red in |- *;  intros; discriminate. intros p' H q; case q. simpl in |- *; red in |- *; intros; discriminate. intros q'; red in |- *; intros H0; case (H q'). replace (2 * q') with (2 * S q' - 2). rewrite <- H0; simpl in |- *; auto. repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *; auto. simpl in |- *; repeat rewrite (fun x y => plus_comm x (S y)); simpl in |- *;  auto. case q'; simpl in |- *; auto. Qed. ```
Tail-recursive mult
``` ```
`tail_mult` is an alternative definition for `mult` which is tail-recursive, whereas `mult` is not. This can be useful when extracting programs.
``` Fixpoint mult_acc (s:nat) m n {struct n} : nat :=   match n with   | O => s   | S p => mult_acc (tail_plus m s) m p   end. Lemma mult_acc_aux : forall n m p, m + n * p = mult_acc m p n. Proof. induction n as [| p IHp]; simpl in |- *; auto. intros s m; rewrite <- plus_tail_plus; rewrite <- IHp. rewrite <- plus_assoc_reverse; apply (f_equal2 (A1:=nat) (A2:=nat)); auto. rewrite plus_comm; auto. Qed. Definition tail_mult n m := mult_acc 0 m n. Lemma mult_tail_mult : forall n m, n * m = tail_mult n m. Proof. intros; unfold tail_mult in |- *; rewrite <- mult_acc_aux; auto. Qed. ```
`TailSimpl` transforms any `tail_plus` and `tail_mult` into `plus` and `mult` and simplify
``` Ltac tail_simpl :=   repeat rewrite <- plus_tail_plus; repeat rewrite <- mult_tail_mult;    simpl in |- *. ```