Library zoo.common.math

From Stdlib Require Export
  ZifyNat.

From stdpp Require Export
  numbers.

From zoo Require Import
  prelude.
From zoo Require Import
  relations.
From zoo Require Import
  options.

Section nat.
  #[global] Instance b2n_inj :
    Inj (=) (=) Nat.b2n.

  Definition nat_elim {A} (x : A) f n :=
    match n with
    | 0 ⇒
        x
    | S n ⇒
        f n
    end.
  #[global] Arguments nat_elim _ _ _ !_ / : assert.

  #[global] Instance ge_partialorder :
    PartialOrder ge.

  #[global] Instance le_initial : Initial (≤) :=
    {|initial := 0
    ; initial_lb := Nat.le_0_l
    |}.

  Lemma minus_mod_1 a b n :
    b ≤ a →
    b `mod` n ≤ a `mod` n →
    (a `mod` n - b `mod` n) `mod` n = (a - b) `mod` n.
  Lemma minus_mod_1' a b n :
    n ≠ 0 →
    b ≤ a →
    b `mod` n ≤ a `mod` n →
    a `mod` n - b `mod` n = (a - b) `mod` n.
  Lemma minus_mod_1'' a b n :
    n ≠ 0 →
    a `mod` n ≤ (a + b) `mod` n →
    (a + b) `mod` n - a `mod` n = b `mod` n.
  Lemma minus_mod_2 a b n :
    n ≠ 0 →
    a ≤ b →
    b `mod` n ≤ a `mod` n →
    a `mod` n - b `mod` n = (n - (b - a) `mod` n) `mod` n.
End nat.

Notation "(≥)" :=
  Z.ge
( only parsing
) : Z_scope.

Section Z.
  #[local] Open Scope Z_scope.

  Lemma Z_rem_mod x y :
    0 ≤ x →
    0 ≤ y →
    x `rem` y = x `mod` y.
End Z.

Section Qp_of_nat.
  Implicit Types n : nat.

  Definition Qp_of_nat :=
    pos_to_Qp ∘ Pos.of_nat.

  Lemma Qp_of_nat_1 :
    Qp_of_nat 1 = 1%Qp.
  Lemma Qp_of_nat_S n :
    n ≠ 0 →
    Qp_of_nat (S n) = (1 + Qp_of_nat n)%Qp.
End Qp_of_nat.