Library zoo.common.math

Require Export Stdlib.micromega.ZifyNat.

Require Export stdpp.numbers.

Require Import zoo.prelude.
Require Import zoo.common.relations.
Require Import zoo.options.

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

  Definition nat۰elim {A} (x : A) f n :=
    match n with
    | 0 ⇒
        x
    | ˖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₁ 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₁' 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₁'' 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₂ 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 Type 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 ˖n = (1 + Qp۰of_nat n)%Qp.
End Qp۰of_nat.