Library More_nat

Require Import Arith.
Require Import ArithRing.
Require Import Compare_dec.
Require Import Omega.
Require Import Max.

Set Implicit Arguments.

Fixpoint power (base exp:nat){struct exp}:nat :=
  match exp with 0 => 1
               | S exp' => base * (power base exp')
  end.

Notation "n ^ p" := (power n p):nat_scope.

Lemma power_of_1 : forall p, power 1 p = 1.
 induction p; simpl.
 auto.
 rewrite IHp;auto.
Qed.
 
Goal forall a b, 0 < power (S a) b.
 induction b.
 simpl;auto.
 simpl.
 auto with arith.
Save power_positive.

Lemma pred_of_power : forall b e, pred (power (S b) (S e)) =
                                  (power (S b) e)*b +
                                  pred (power (S b) e).
 simpl.
 intros;generalize ((S b) ^e).
 destruct n.
 simpl.
 rewrite mult_0_r.
 simpl;auto.
 rewrite (mult_comm b (S n)).
simpl.
ring_nat.
Qed.

Lemma get_predecessor : forall (n:nat), 0 < n -> {p:nat | n = S p}.
 intro n; case n.
 intro ; absurd (0<0); auto with arith.
 intro n0; exists n0;auto.
Qed.

Ltac pred_exhib H name :=
  match type of H
       with O < ?n =>
         case (get_predecessor H); intro name; intro
  end.

Lemma Euc1 : forall b q q' r r', 0 < b ->
                                  q*b + r = q'*b + r' ->
                                  r < b -> r' < b -> q = q'.
intros; case (lt_eq_lt_dec q q').
destruct 1.
assert (S q <= q').
auto with arith.
assert ((S q)*b + r <= q' *b + r).
apply plus_le_compat_r.
apply mult_le_compat_r.
auto.
simpl in H4.
rewrite <- plus_assoc in H4.
rewrite H0 in H4.
omega.
auto.
intro.
assert (S q' <= q).
auto with arith.
assert ((S q')*b + r <= q *b + r).
apply plus_le_compat_r.
apply mult_le_compat_r.
auto.
simpl in H4.
rewrite <- plus_assoc in H4.
rewrite H0 in H4.
omega.
Qed.

Lemma Euc2 : forall b q q' r r', 0 < b ->
               q*b+r = q'*b+r' -> r < b -> r' < b -> r =r'.
 intros.
 rewrite (Euc1 q q' H H0 H1 H2) in H0.
 omega.
Qed.

Lemma max_le_regR : forall n p q, p <= q -> max p n <= max q n.
  intros; case (max_dec p n).
 intro e;rewrite e.
 apply le_trans with q.
 auto.
  apply le_max_l.
 intro e;rewrite e.
 apply le_max_r.
Qed.

Lemma max_le_regL : forall n p q, p <= q -> max n p <= max n q.
  intros; rewrite (max_comm n p);rewrite (max_comm n q).
  apply max_le_regR.
  auto.
Qed.

Lemma lt_lt_Sn : forall a b c, a < b -> b < S c -> a < c.
 eauto with arith.
Qed.

 

Index
This page has been generated by coqdoc