proposition: Lemma div_gamma_pos {gamma}{Hgamma : Strategy gamma} : forall (p:positive) q r, N.pos_div_eucl p (N.pos (gamma p)) = (q, r) -> 3 < p -> (0 < q)%N.
proof: Proof. destruct q; [ | reflexivity]. intros r H H0;assert (H1 : p = N2pos r) by (apply (N_pos_div_eucl_q0 _ _ _ H);auto). destruct (Pos.lt_irrefl p). transitivity (gamma p). - rewrite H1 at 1. generalize (N.pos_div_eucl_remainder p (N.pos (gamma p))); rewrite H; cbn. intros H2; destruct r. + apply gamma_gt; auto. + rewrite <- pos2N_inj_lt in H2; cbn; auto with chains. - apply gamma_lt;auto with chains. Qed.
imports: Arith NArith Pow Compatibility More_on_positive