(* Contribution to the Coq Library   V6.3 (July 1999)                    *)

(****************************************************************************)
(*                 The Calculus of Inductive Constructions                  *)
(*                                                                          *)
(*                                Projet Coq                                *)
(*                                                                          *)
(*                     INRIA                        ENS-CNRS                *)
(*              Rocquencourt                        Lyon                    *)
(*                                                                          *)
(*                                Coq V5.10                                 *)
(*                              Nov 25th 1994                               *)
(*                                                                          *)
(****************************************************************************)
(*                            Nat_complements.v                             *)
(****************************************************************************)
Require Import Arith.
Require Import Compare_dec.

(****************)
Lemma eq_gt_O_dec : forall n : nat, {n = 0} + {n > 0}.

(* Goal: forall n : nat, sumbool (@eq nat n O) (gt n O) *)
simple destruct n; auto with arith.
Qed.

(****************)
Lemma mult_commut : forall n m : nat, n * m = m * n.

(* Goal: forall n m : nat, @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n) *)
intros; elim n; simpl in |- *.
(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
auto with arith.
(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
intros; rewrite H; elim mult_n_Sm; auto with arith.
Qed.

(***************)
Lemma mult_neutr : forall n : nat, 1 * n = n.

(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
unfold mult in |- *; auto with arith.
Qed.

(********************)
Lemma technical_lemma :
 forall y m : nat, S (y * m + (y + m) + m) = S y * m + (S y + m).

(* Goal: forall y m : nat, @eq nat (S (Init.Nat.add (Init.Nat.add (Init.Nat.mul y m) (Init.Nat.add y m)) m)) (Init.Nat.add (Init.Nat.mul (S y) m) (Init.Nat.add (S y) m)) *)
intros; simpl in |- *; elim (plus_comm m (y * m + (y + m))).
(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
rewrite (plus_assoc m (y * m) (y + m)); auto with arith.
Qed.

(**************)
Lemma lt_minus2 : forall n m : nat, n < m -> 0 < m - n.
(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
simple induction 1; intros; elim minus_Sn_m; auto with arith.
Qed.

(***************)
Lemma minus_n_Sm : forall n m : nat, m < n -> pred (n - m) = n - S m.

(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
simple induction 1; intros; elim minus_Sn_m; auto with arith.
Qed.

(************)
Lemma lt_succ : forall n m : nat, n <= S m -> {n <= m} + {n = S m}.

(* Goal: @eq nat O (Init.Nat.mul m O) *)
(* Goal: forall (n : nat) (_ : @eq nat (Init.Nat.mul n m) (Init.Nat.mul m n)), @eq nat (Init.Nat.add m (Init.Nat.mul n m)) (Init.Nat.mul m (S n)) *)
intros; elim (le_lt_eq_dec n (S m) H); auto with arith.
Qed.