Module LibPos

Require Export Coqlib.
Require Export ZArith.
Require Import Tactics.
Load Param.

Lemma Plt_rev_trans :forall a b,
Plt b a ->
forall c, Plt c b -> Plt c a.

Proof.

Lemma Ple_Plt_trans:
forall (p q r: positive), Ple p q -> Plt q r -> Plt p r.

Proof.

Lemma Ple_antisym : forall p q, Ple p q -> Ple q p -> p = q.

Proof.

Section Bounded_gt.

Variable p : positive.

Inductive bounded_gt : positive -> positive -> Prop :=
| bounded_gt_intro : forall a b,
  Plt b a -> Plt a p -> bounded_gt a b.

Function bound_gt (q : positive) : nat :=
  match (Zpos p - Zpos q)%Z with
    | Zpos r => nat_of_P r
    | _ => O
  end.

Theorem bounded_gt_wf : well_founded bounded_gt.

Proof.

End Bounded_gt.

Section Bounded_exists.
Variable p : positive -> bool.

Lemma bounded_exists : forall n,
{j | Plt j n /\ p j = true} + {forall j, Plt j n -> p j = false}.

Proof.

End Bounded_exists.

Definition lcm a b := a * (b / Zgcd a b).

Lemma lcm_positive : forall a, 0 < a -> forall b, 0 < b -> 0 < lcm a b.

Proof.

Theorem lcm_prop : forall a, 0 < a -> forall b, 0 < b -> forall q,
(a | q) -> (b | q) -> (lcm a b | q).

Proof.

Lemma lcm_divides_left : forall a b, (a | lcm a b).

Proof.

Lemma lcm_divides_right : forall a b, 0 < b -> (b | lcm a b).

Proof.

Lemma incr_align : forall a, (0 < a) -> forall p, {q | p <= q /\ (a | q)}.

Proof.

           Section Bounded.

             Variable align : Z.
             Hypothesis align_pos : 0 < align.

             Variable low_bound high_bound : Z.

             Variable f : Z -> bool.

             Definition bounded_offset : {z | low_bound <= z /\ (align | z) /\ (high_bound <= z \/ f z = true)}.

Proof.

End Bounded.