Library additions.Strategies

A strategy is any function of type positive positive such that, if , then .

Require Import Arith NArith Pow Compatibility More_on_positive.
Open Scope positive_scope.

Open Scope positive_scope.
Class Strategy (gamma : positive positive):=
  {
  gamma_lt : p:positive, 3 < p gamma p < p;
  gamma_gt : p:positive, 3 < p 1 < gamma p
  }.

Ltac gamma_bounds gamma i H1 H2 :=
  assert (H1 : 1 < gamma i) by (apply gamma_gt;auto with chains);
  assert (H2 : gamma i < i) by (apply gamma_lt; auto with chains).

Lemma div_gamma_pos {gamma}{Hgamma : Strategy gamma}
: (p:positive) q r,
    N.pos_div_eucl p (N.pos (gamma p)) = (q, r)
    3 < p
    (0 < q)%N.