Library additions.Strategies

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.