(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
(*              Rocquencourt         Orsay          Lyon                    *)
(*                                                                          *)
(*                                 Coq V6.2                                 *)
(*                               May 1st 1998                               *)
(*                                                                          *)
(****************************************************************************)
(*                                  Mult.v                                  *)
(****************************************************************************)

(* Omega solve only linear goals. It fails on goals with "mult" *)
(* except if one of the multiplicands is a constant             *)
(* as in mult_n_1 and mult_1_n                                  *)

Require Omega.
Require Le_omega.
Require Lt_omega.
Require Plus_omega.
Require Minus_omega.

(**********************************************************)
(* Multiplication                                         *)
(**********************************************************)

Lemma mult_plus_distr : 
      (n,m,p:nat)((mult (plus n m) p)=(plus (mult n p) (mult m p))).
Proof.
Intros; Elim n; Simpl; Intros; Trivial.
Elim plus_assoc_l; Elim H; Auto.
Qed.
Hint mult_plus_distr.

Lemma mult_minus_distr : (n,m,p:nat)((mult (minus n m) p)=(minus (mult n p) (mult m p))).
Proof.
Intros; Pattern n m; Apply nat_double_ind; Simpl; Intros; Trivial.
Elim minus_plus_simpl; Auto.
Qed.
Hint mult_minus_distr.

Lemma mult_O_le : (n,m:nat)(m=O)\/(le n (mult m n)).
Proof.
Induction m; Simpl; Auto.
Qed.
Hint mult_O_le.

Lemma mult_assoc_r : (n,m,p:nat)((mult (mult n m) p) = (mult n (mult m p))).
Proof.
Intros; Elim n; Intros; Simpl; Auto.
Rewrite mult_plus_distr.
Elim H; Auto.
Qed.
Hint mult_assoc_r.

Lemma mult_assoc_l : (n,m,p:nat)(mult n (mult m p)) = (mult (mult n m) p).
Proof.
Auto.
Qed.
Hint mult_assoc_l.

Lemma mult_1_n : (n:nat)(mult (S O) n)=n.
Proof.
Intros; Omega.
Qed.
Hint mult_1_n.

Lemma mult_sym : (n,m:nat)(mult n m)=(mult m n).
Proof.
Intros; Elim n; Intros; Simpl; Auto.
Elim mult_n_Sm.
Elim H; Apply plus_sym.
Qed.
Hint mult_sym.

Lemma mult_n_1 : (n:nat)(mult n (S O))=n.
Proof.
Intros; Omega.
Qed.
Hint mult_n_1.


(* $Id: Mult_omega.v,v 1.1 1998/07/02 13:22:16 loiseleu Exp $ *)
