From Coq Require Import Arith NArith Lia Recdef.
From additions Require Import Pow Compatibility Wf_transparent.
Open Scope positive_scope.
Import Monoid_def.

Definition pos_eq_dec : ∀ p p':positive, {p = p'}+{p ≠ p'}.

Lemma N_0_le_n: ∀ n:N, (0 ≤ n)%N.

Lemma Pos_to_nat_neq_0 : ∀ p, Pos.to_nat p ≠ 0%nat.

#[global] Hint Resolve Pos_to_nat_neq_0 : chains.

Lemma Npos_diff_zero : ∀ p, N.pos p ≠ 0%N.

Lemma Npos_gt_0 : ∀ p, (0 < N.pos p)%N.

#[global] Hint Resolve Npos_diff_zero Npos_gt_0 : chains.

Lemma pos2N_inj_lt : ∀ n p, (n < p)%positive ↔ (N.pos n < N.pos p)%N.

Lemma pos2N_inj_add : ∀ n p, N.pos (n + p) = (N.pos n + N.pos p)%N.

Ltac pos2nat_inj_tac :=
  repeat (rewrite Pos2Nat.inj_add || rewrite Pos2Nat.inj_mul ||
          rewrite Pos2Nat.inj_lt || rewrite Pos2Nat.inj_le).

Lemma Pos2Nat_le_1_p : ∀ p, (1 ≤ Pos.to_nat p)%nat.

Lemma N_le_1_pos : ∀ p, (1 ≤ N.pos p)%N.

Lemma pos_le_mul : ∀ p q , (p ≤ p × q)%positive.

Lemma pos_lt_mul : ∀ p q , (1 < q → p < p × q)%positive.

Lemma Pos2Nat_le_n_pn :
  ∀ p q,
    (Pos.to_nat p ≤ Pos.to_nat p × Pos.to_nat q)%nat.

#[global] Hint Resolve Pos2Nat_le_1_p : chains.

Definition N2pos (n:N) : positive :=
 match n with 0%N ⇒ xH | Npos p ⇒ p end.

Lemma N2pos_pos :
  ∀ i, N2pos (Npos i) = i.

Lemma N_pos_N2pos : ∀ n, 0%N ≠ n → n = Npos (N2pos n).

Lemma N2pos_lt_switch : ∀ n p, (0%N < n)%N →
                                     ( (N.pos p < n)%N ↔ (p < N2pos n)%positive).

Ltac N2pos_simpl x := simpl (N2pos (N.pos x)) in ×.

Ltac N2pos_destruct t y :=
 destruct t as [| y] ; [try (discriminate || contradiction) | N2pos_simpl y].

Lemma N2pos_lt_switch2 : ∀ n p, (0%N < n)%N →
                                      ((N2pos n < p)%positive
                                       ↔ (n < N.pos p)%N).

Lemma pos_lt_wf : well_founded Pos.lt.

Fixpoint exact_log2(p:positive) : option positive :=
match p with
  | 1%positive | xI _ ⇒ None
  | 2%positive ⇒ Some xH
  | xO q ⇒ match exact_log2 q with
              | Some l ⇒ Some (l+1)%positive
              | _ ⇒ None
            end
end.

Lemma exact_log2xOx0 :
  ∀ p i, exact_log2 (xO p) = Some i →
              exact_log2 (xO (xO p)) = Some (i+1)%positive.

Lemma exact_log2_spec :
  ∀ p i: positive, exact_log2 p = Some i → p = (2 ^ i)%positive.

Lemma positive_4step_ind : ∀ P : positive → Prop,
   P 1%positive → P 2%positive → P 3%positive →
  (∀ p, P p → P (xO (xO p)) ∧ P (xI (xO p)) ∧ P (xO (xI p)) ∧
               P (xI (xI p))) →
  ∀ p, P p.

Lemma pos_gt_3 : ∀ p:positive,
  p ≠ 1 → p ≠ 3 → exact_log2 p = None → 3 < p.

#[global] Hint Resolve pos_gt_3 : chains.

Lemma pos_div_eucl_quotient_pos : ∀ a b q r,
                                    N.pos_div_eucl a b = (q, r) →
                                    (b ≤ N.pos a)%N →
                                    b ≠ 0%N →
                                    (q ≠ 0%N).

Lemma pos_div_eucl_quotient_lt : ∀ a b q r,
                                   N.pos_div_eucl a b = (q, r) →
                                   (1 < b)%N →
                                   (q < N.pos a)%N.

Lemma N_pos_div_eucl_divides : ∀ i b q,
                                 N.pos_div_eucl i (N.pos b) = (q, 0%N) →
                                 (b × N2pos q)%positive = i.

 Lemma N_pos_div_eucl_rest : ∀ i b q r,
                               N.pos_div_eucl i (N.pos b) = (q, r) →
                               (0 < r)%N → (0 < q)%N →
                               (b × N2pos q + N2pos r)%positive = i.

 Lemma N_pos_div_eucl_q0 : ∀ i b r,
                             N.pos_div_eucl i (N.pos b) = (0%N, r) →
                             i = N2pos r.

Lemma lt_S_2i :
∀ i j:nat, (i < j → 2 × i + 1 < 2 × j)%nat.

Lemma N_le_mul_pos : ∀ q p, (q ≤ q × N.pos p)%N.

Ltac quotient_small div_equation H :=
  match type of div_equation with
    (N.pos_div_eucl ?a ?b = (?q,?r)) ⇒
    assert (H : (q < N.pos a)%N);
    [apply (pos_div_eucl_quotient_lt _ _ _ _ div_equation); auto|]
  end.

Ltac rest_small div_equation H :=
  match type of div_equation with
    (N.pos_div_eucl ?a ?b = (?q,?r)) ⇒
    let H0 := fresh "H" in
    assert (H : (r < b)%N);
    [generalize (N.pos_div_eucl_remainder a b); simpl; intro H0;
     rewrite div_equation in H0; apply H0 ; try discriminate| ]
  end.