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.