phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/numbers.v *)
Instance add_left_id : LeftId (=) 0 N.add
:= N.add_0_l.
(* stdpp/numbers.v *)
Instance add_right_id : RightId (=) 0 N.add
:= N.add_0_r.
(* stdpp/numbers.v *)
Instance sub_right_id : RightId (=) 0 N.sub
:= N.sub_0_r.
(* stdpp/numbers.v *)
Instance mul_assoc' : Assoc (=) N.mul
:= N.mul_assoc.
(* stdpp/numbers.v *)
Instance mul_comm' : Comm (=) N.mul
:= N.mul_comm.
(* stdpp/numbers.v *)
Instance mul_left_id : LeftId (=) 1 N.mul
:= N.mul_1_l.
(* stdpp/numbers.v *)
Instance mul_right_id : RightId (=) 1 N.mul
:= N.mul_1_r.
(* stdpp/numbers.v *)
Instance mul_left_absorb : LeftAbsorb (=) 0 N.mul
:= N.mul_0_l.
(* stdpp/numbers.v *)
Instance mul_right_absorb : RightAbsorb (=) 0 N.mul
:= N.mul_0_r.
(* stdpp/numbers.v *)
Instance div_right_id : RightId (=) 1 N.div
:= N.div_1_r.
(* stdpp/numbers.v *)
Instance pos_inj : Inj (=) (=) N.pos.
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Instance eq_dec : EqDecision N
:= N.eq_dec.
(* stdpp/numbers.v *)
Instance le_dec : RelDecision N.le
:= λ x y,
    match N.compare x y with Gt => right _ | _ => left _ end.
(* stdpp/numbers.v *)
Instance lt_dec : RelDecision N.lt
:= λ x y,
    match N.compare x y with Lt => left _ | _ => right _ end.
(* stdpp/numbers.v *)
Instance inhabited : Inhabited N
:= populate 1%N.
(* stdpp/numbers.v *)
Instance lt_pi x y : ProofIrrel (x < y)%N.
Proof. unfold N.lt. apply _. Qed.
(* stdpp/numbers.v *)
Instance le_po : PartialOrder (≤)%N.
Proof.
    repeat split; red; [apply N.le_refl | apply N.le_trans | apply N.le_antisymm].
  Qed.
(* stdpp/numbers.v *)
Instance le_total : Total (≤)%N.
Proof. repeat intro; lia. Qed.
(* stdpp/numbers.v *)
Lemma lt_wf_0_projected {B} (f : B → N) : well_founded (λ x y, f x < f y).
Proof. by apply (wf_projected (<) f), lt_wf_0. Qed.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z"
:= (x ≤ y ∧ y ≤ z) : Z_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y < z"
:= (x ≤ y ∧ y < z) : Z_scope.
(* stdpp/numbers.v *)
Notation "x < y < z"
:= (x < y ∧ y < z) : Z_scope.
(* stdpp/numbers.v *)
Notation "x < y ≤ z"
:= (x < y ∧ y ≤ z) : Z_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z ≤ z'"
:= (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Z_scope.
(* stdpp/numbers.v *)
Notation "(≤)"
:= Z.le (only parsing) : Z_scope.
(* stdpp/numbers.v *)
Notation "(<)"
:= Z.lt (only parsing) : Z_scope.
(* stdpp/numbers.v *)
Instance add_assoc' : Assoc (=) Z.add
:= Z.add_assoc.
(* stdpp/numbers.v *)
Instance add_comm' : Comm (=) Z.add
:= Z.add_comm.
(* stdpp/numbers.v *)
Instance add_left_id : LeftId (=) 0 Z.add
:= Z.add_0_l.
(* stdpp/numbers.v *)
Instance add_right_id : RightId (=) 0 Z.add
:= Z.add_0_r.
(* stdpp/numbers.v *)
Instance sub_right_id : RightId (=) 0 Z.sub
:= Z.sub_0_r.
(* stdpp/numbers.v *)
Instance mul_assoc' : Assoc (=) Z.mul
:= Z.mul_assoc.
(* stdpp/numbers.v *)
Instance mul_comm' : Comm (=) Z.mul
:= Z.mul_comm.
(* stdpp/numbers.v *)
Instance mul_left_id : LeftId (=) 1 Z.mul
:= Z.mul_1_l.
(* stdpp/numbers.v *)
Instance mul_right_id : RightId (=) 1 Z.mul
:= Z.mul_1_r.
(* stdpp/numbers.v *)
Instance mul_left_absorb : LeftAbsorb (=) 0 Z.mul
:= Z.mul_0_l.
(* stdpp/numbers.v *)
Instance mul_right_absorb : RightAbsorb (=) 0 Z.mul
:= Z.mul_0_r.
(* stdpp/numbers.v *)
Instance div_right_id : RightId (=) 1 Z.div
:= Z.div_1_r.
(* stdpp/numbers.v *)
Instance pos_inj : Inj (=) (=) Z.pos.
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Instance neg_inj : Inj (=) (=) Z.neg.
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Instance eq_dec: EqDecision Z
:= Z.eq_dec.
(* stdpp/numbers.v *)
Instance le_dec: RelDecision Z.le
:= Z_le_dec.
(* stdpp/numbers.v *)
Instance lt_dec: RelDecision Z.lt
:= Z_lt_dec.
(* stdpp/numbers.v *)
Instance ge_dec: RelDecision Z.ge
:= Z_ge_dec.
(* stdpp/numbers.v *)
Instance gt_dec: RelDecision Z.gt
:= Z_gt_dec.
(* stdpp/numbers.v *)
Instance inhabited: Inhabited Z
:= populate 1.
(* stdpp/numbers.v *)
Instance lt_pi x y : ProofIrrel (x < y).
Proof. unfold Z.lt. apply _. Qed.
(* stdpp/numbers.v *)
Instance le_po : PartialOrder (≤).
Proof.
    repeat split; red; [apply Z.le_refl | apply Z.le_trans | apply Z.le_antisymm].
  Qed.
(* stdpp/numbers.v *)
Instance le_total: Total Z.le.
Proof. repeat intro; lia. Qed.
(* stdpp/numbers.v *)
Lemma lt_wf_projected {B} (f : B → Z) z : well_founded (λ x y, z ≤ f x < f y).
Proof. by apply (wf_projected (λ x y, z ≤ x < y) f), lt_wf. Qed.
(* stdpp/numbers.v *)
Lemma pow_pred_r n m : 0 < m → n * n ^ (Z.pred m) = n ^ m.
Proof.
    intros. rewrite <-Z.pow_succ_r, Z.succ_pred; [done|]. by apply Z.lt_le_pred.
  Qed.
(* stdpp/numbers.v *)
Lemma quot_range_nonneg k x y : 0 ≤ x < k → 0 < y → 0 ≤ x `quot` y < k.
Proof.
    intros [??] ?.
    destruct (decide (y = 1)); subst; [rewrite Z.quot_1_r; auto |].
    destruct (decide (x = 0)); subst; [rewrite Z.quot_0_l; auto with lia |].
    split; [apply Z.quot_pos; lia|].
    trans x; auto. apply Z.quot_lt; lia.
  Qed.
(* stdpp/numbers.v *)
Lemma mod_pos x y : 0 < y → 0 ≤ x `mod` y.
Proof. apply Z.mod_pos_bound. Qed.
(* stdpp/numbers.v *)
Lemma succ_pred_induction y (P : Z → Prop) :
    P y →
    (∀ x, y ≤ x → P x → P (Z.succ x)) →
    (∀ x, x ≤ y → P x → P (Z.pred x)) →
    (∀ x, P x).
Proof. intros H0 HS HP. by apply (Z.order_induction' _ _ y). Qed.
(* stdpp/numbers.v *)
Lemma mod_in_range q a c :
    q * c ≤ a < (q + 1) * c →
    a `mod` c = a - q * c.
Proof. intros ?. symmetry. apply Z.mod_unique_pos with q; lia. Qed.
(* stdpp/numbers.v *)
Lemma ones_spec n m:
    0 ≤ m → 0 ≤ n →
    Z.testbit (Z.ones n) m = bool_decide (m < n).
Proof.
    intros. case_bool_decide.
    - by rewrite Z.ones_spec_low by lia.
    - by rewrite Z.ones_spec_high by lia.
  Qed.
(* stdpp/numbers.v *)
Lemma bounded_iff_bits_nonneg k n :
    0 ≤ k → 0 ≤ n →
    n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
Proof.
    intros. destruct (decide (n = 0)) as [->|].
    { naive_solver eauto using Z.bits_0, Z.pow_pos_nonneg with lia. }
    split.
    { intros Hb%Z.log2_lt_pow2 l Hl; [|lia]. apply Z.bits_above_log2; lia. }
    intros Hl. apply Z.nle_gt; intros ?.
    assert (Z.testbit n (Z.log2 n) = false) as Hbit.
    { apply Hl, Z.log2_le_pow2; lia. }
    by rewrite Z.bit_log2 in Hbit by lia.
  Qed.
(* stdpp/numbers.v *)
(* Goals of the form [0 ≤ n ≤ 2^k] appear often. So we also define the
  derived version [Z_bounded_iff_bits_nonneg'] that does not require
  proving [0 ≤ n] twice in that case. *)
Lemma bounded_iff_bits_nonneg' k n :
    0 ≤ k → 0 ≤ n →
    0 ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = false.
Proof. intros ??. rewrite <-bounded_iff_bits_nonneg; lia. Qed.
(* stdpp/numbers.v *)
Lemma bounded_iff_bits k n :
    0 ≤ k →
    -2^k ≤ n < 2^k ↔ ∀ l, k ≤ l → Z.testbit n l = bool_decide (n < 0).
Proof.
    intros Hk.
    case_bool_decide; [ | rewrite <-bounded_iff_bits_nonneg; lia].
    assert(n = - Z.abs n)%Z as -> by lia.
    split.
    { intros [? _] l Hl.
      rewrite Z.bits_opp, negb_true_iff by lia.
      apply bounded_iff_bits_nonneg with k; lia. }
    intros Hbit. split.
    - rewrite <-Z.opp_le_mono, <-Z.lt_pred_le.
      apply bounded_iff_bits_nonneg; [lia..|]. intros l Hl.
      rewrite <-negb_true_iff, <-Z.bits_opp by lia.
      by apply Hbit.
    - etrans; [|apply Z.pow_pos_nonneg]; lia.
  Qed.
(* stdpp/numbers.v *)
Lemma add_alt_addcarries a b :
    a + b = Z.lxor (Z.lxor a b) (Z.addcarries a b).
Proof.
    unfold Z.addcarries.
    by rewrite Z.lxor_comm, Z.lxor_assoc, Z.lxor_nilpotent, Z.lxor_0_r.
  Qed.
(* stdpp/numbers.v *)
Lemma add_spec a b i :
    Z.testbit (a + b) i = xorb
      (xorb (Z.testbit a i) (Z.testbit b i))
      (Z.testbit (Z.addcarries a b) i).
Proof. by rewrite Z.add_alt_addcarries, !Z.lxor_spec. Qed.
(* stdpp/numbers.v *)
Lemma addcarries_spec a b i :
    Z.testbit (Z.addcarries a b) i =
      Z.testbit a (i-1) && Z.testbit b (i-1) ||
      (Z.testbit a (i-1) || Z.testbit b (i-1)) && negb (Z.testbit (a+b) (i-1)).
Proof.
    destruct (decide (0 < i)).
    - rewrite Z.testbit_addcarries_pos by lia.
      rewrite Z.add_spec.
      by destruct (Z.testbit a (i - 1)), (Z.testbit b (i - 1)),
        (Z.testbit (Z.addcarries a b) (i - 1)).
    - rewrite !(Z.testbit_neg_r _ (i - 1)) by lia; simpl.
      destruct (decide (i = 0)); subst.
      + apply Z.testbit_addcarries_0.
      + by rewrite Z.testbit_neg_r by lia.
  Qed.
(* stdpp/numbers.v *)
Lemma opp_pow2_spec n i :
    0 ≤ n →
    Z.testbit (- 2 ^ n) i = bool_decide (n ≤ i).
Proof.
    intros. destruct (decide (0 ≤ i)).
    - rewrite Z.bits_opp, <-Z.ones_equiv, Z.ones_spec by done.
      repeat case_bool_decide; lia.
    - rewrite Z.testbit_neg_r by lia. case_bool_decide; lia.
  Qed.
(* stdpp/numbers.v *)
Lemma add_pow2_spec_low m n i :
    0 ≤ n →
    i < n →
    Z.testbit (m + 2 ^ n) i = Z.testbit m i.
Proof.
    intros. rewrite <-(Z.mod_pow2_bits_low (_ + _) n i) by lia.
    rewrite <-Zplus_mod_idemp_r, Z_mod_same_full, Z.add_0_r.
    by rewrite Z.mod_pow2_bits_low by lia.
  Qed.
(* stdpp/numbers.v *)
Lemma sub_pow2_spec_low m n i :
    0 ≤ n →
    i < n →
    Z.testbit (m - 2 ^ n) i = Z.testbit m i.
Proof.
    intros. rewrite <-Z.add_opp_r.
    rewrite <-(Z.mod_pow2_bits_low (_ + _) n i), Z.add_opp_r by lia.
    rewrite <-Zminus_mod_idemp_r, Z_mod_same_full, Z.sub_0_r.
    by rewrite Z.mod_pow2_bits_low by lia.
  Qed.
(* stdpp/numbers.v *)
Lemma add_pow2_spec_top m n :
    0 ≤ n →
    Z.testbit (m + 2 ^ n) n = negb (Z.testbit m n).
Proof.
    intros. rewrite Z.add_spec, Z.addcarries_spec.
    rewrite Z.add_pow2_spec_low, Z.pow2_bits_true, Z.pow2_bits_false by lia.
    destruct (Z.testbit m n), (Z.testbit m (n - 1)); done.
  Qed.
(* stdpp/numbers.v *)
Lemma sub_pow2_spec_top m n :
    0 ≤ n →
    Z.testbit (m - 2 ^ n) n = negb (Z.testbit m n).
Proof.
    intros. rewrite <-Z.add_opp_r, Z.add_spec, Z.addcarries_spec, Z.add_opp_r.
    rewrite Z.sub_pow2_spec_low, !Z.opp_pow2_spec by lia.
    repeat case_bool_decide; try lia;
      by destruct (Z.testbit m n), (Z.testbit m (n - 1)).
  Qed.
(* stdpp/numbers.v *)
Lemma sub_pow2_spec_high m n i :
    0 ≤ n →
    0 ≤ m < 2 ^ Z.succ n →
    n ≤ i →
    Z.testbit (m - 2 ^ n) i = negb (Z.testbit m n).
Proof.
    intros Hn Hm ?. rewrite <- Z.sub_pow2_spec_top by lia.
    rewrite Z.pow_succ_r in Hm by done.
    rewrite !(proj1 (Z.bounded_iff_bits n (m - 2 ^ n) Hn)) by lia. done.
  Qed.
(* stdpp/numbers.v *)
Lemma add_nocarry_lor a b :
    Z.land a b = 0 →
    a + b = Z.lor a b.
Proof. intros ?. rewrite <-Z.lxor_lor by done. by rewrite Z.add_nocarry_lxor. Qed.
(* stdpp/numbers.v *)
Lemma opp_lnot a : -a - 1 = Z.lnot a.
Proof. pose proof (Z.add_lnot_diag a). lia. Qed.
(* stdpp/numbers.v *)
Instance inj' : Inj (=) (=) Z.of_nat.
Proof. intros n1 n2. apply Nat2Z.inj. Qed.
(* stdpp/numbers.v *)
Lemma divide n m : (Z.of_nat n | Z.of_nat m) ↔ (n | m)%nat.
Proof.
    split.
    - rewrite <-(Nat2Z.id m) at 2; intros [i ->]; exists (Z.to_nat i). lia.
    - intros [i ->]. exists (Z.of_nat i). by rewrite Nat2Z.inj_mul.
  Qed.
(* stdpp/numbers.v *)
Lemma inj_div x y : Z.of_nat (x `div` y) = (Z.of_nat x) `div` (Z.of_nat y).
Proof.
    destruct (decide (y = 0%nat)); [by subst; destruct x |].
    apply Z.div_unique with (Z.of_nat $ x `mod` y)%nat.
    { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
      apply Nat.mod_bound_pos; lia. }
    by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
  Qed.
(* stdpp/numbers.v *)
Lemma inj_mod x y : Z.of_nat (x `mod` y) = (Z.of_nat x) `mod` (Z.of_nat y).
Proof.
    destruct (decide (y = 0%nat)); [by subst; destruct x |].
    apply Z.mod_unique with (Z.of_nat $ x `div` y)%nat.
    { left. rewrite <-(Nat2Z.inj_le 0), <-Nat2Z.inj_lt.
      apply Nat.mod_bound_pos; lia. }
    by rewrite <-Nat2Z.inj_mul, <-Nat2Z.inj_add, <-Nat.div_mod.
  Qed.
(* stdpp/numbers.v *)
Lemma neq_0_pos x : Z.to_nat x ≠ 0%nat → 0 < x.
Proof. by destruct x. Qed.
(* stdpp/numbers.v *)
Lemma neq_0_nonneg x : Z.to_nat x ≠ 0%nat → 0 ≤ x.
Proof. by destruct x. Qed.
(* stdpp/numbers.v *)
Lemma nonpos x : x ≤ 0 → Z.to_nat x = 0%nat.
Proof. destruct x; simpl; auto using Z2Nat.inj_neg. by intros []. Qed.
(* stdpp/numbers.v *)
Lemma inj_pow (x y : nat) : Z.of_nat (x ^ y) = (Z.of_nat x) ^ (Z.of_nat y).
Proof.
    induction y as [|y IH]; [by rewrite Z.pow_0_r, Nat.pow_0_r|].
    by rewrite Nat.pow_succ_r, Nat2Z.inj_succ, Z.pow_succ_r,
      Nat2Z.inj_mul, IH by auto with zpos.
  Qed.
(* stdpp/numbers.v *)
Lemma divide n m :
    0 ≤ n → 0 ≤ m → (Z.to_nat n | Z.to_nat m)%nat ↔ (n | m).
Proof. intros. by rewrite <-Nat2Z.divide, !Z2Nat.id by done. Qed.
(* stdpp/numbers.v *)
Lemma inj_div x y :
    0 ≤ x → 0 ≤ y →
    Z.to_nat (x `div` y) = (Z.to_nat x `div` Z.to_nat y)%nat.
Proof.
    intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
    pose proof (Z.div_pos x y).
    apply (base.inj Z.of_nat). by rewrite Nat2Z.inj_div, !Z2Nat.id by lia.
  Qed.
(* stdpp/numbers.v *)
Lemma inj_mod x y :
    0 ≤ x → 0 ≤ y →
    Z.to_nat (x `mod` y) = (Z.to_nat x `mod` Z.to_nat y)%nat.
Proof.
    intros. destruct (decide (y = Z.of_nat 0%nat)); [by subst; destruct x|].
    pose proof (Z.mod_pos x y).
    apply (base.inj Z.of_nat). by rewrite Nat2Z.inj_mod, !Z2Nat.id by lia.
  Qed.
(* stdpp/numbers.v *)
(* ** [bool_to_Z] *)
Definition bool_to_Z (b : bool) : Z
:=
  if b then 1 else 0.
(* stdpp/numbers.v *)
Lemma bool_to_Z_bound b : 0 ≤ bool_to_Z b < 2.
Proof. destruct b; simpl; lia. Qed.
(* stdpp/numbers.v *)
Lemma bool_to_Z_eq_0 b : bool_to_Z b = 0 ↔ b = false.
Proof. destruct b; naive_solver. Qed.
(* stdpp/numbers.v *)
Lemma bool_to_Z_neq_0 b : bool_to_Z b ≠ 0 ↔ b = true.
Proof. destruct b; naive_solver. Qed.
(* stdpp/numbers.v *)
Lemma bool_to_Z_spec b n : Z.testbit (bool_to_Z b) n = bool_decide (n = 0) && b.
Proof. by destruct b, n. Qed.
(* stdpp/numbers.v *)
Instance inj' : Inj (=) (=) N.of_nat
:= Nat2N.inj.
(* stdpp/numbers.v *)
Instance inj' : Inj (=) (=) N.to_nat
:= N2Nat.inj.
(* stdpp/numbers.v *)
Instance inj' : Inj (=) (=) Pos.to_nat
:= Pos2Nat.inj.
(* stdpp/numbers.v *)
Instance inj' : Inj (=) (=) Pos.of_succ_nat
:= SuccNat2Pos.inj.
(* stdpp/numbers.v *)
Instance inj' : Inj (=) (=) Z.of_N
:= N2Z.inj.
(* stdpp/numbers.v *)
Notation "1"
:= (Q2Qc 1) : Qc_scope.
(* stdpp/numbers.v *)
Notation "2"
:= (1+1) : Qc_scope.
(* stdpp/numbers.v *)
Notation "- 1"
:= (Qcopp 1) : Qc_scope.
(* stdpp/numbers.v *)
Notation "- 2"
:= (Qcopp 2) : Qc_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z"
:= (x ≤ y ∧ y ≤ z) : Qc_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y < z"
:= (x ≤ y ∧ y < z) : Qc_scope.
(* stdpp/numbers.v *)
Notation "x < y < z"
:= (x < y ∧ y < z) : Qc_scope.
(* stdpp/numbers.v *)
Notation "x < y ≤ z"
:= (x < y ∧ y ≤ z) : Qc_scope.
(* stdpp/numbers.v *)
Notation "x ≤ y ≤ z ≤ z'"
:= (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope.
(* stdpp/numbers.v *)
Notation "(≤)"
:= Qcle (only parsing) : Qc_scope.
(* stdpp/numbers.v *)
Notation "(<)"
:= Qclt (only parsing) : Qc_scope.
(* stdpp/numbers.v *)
Instance Qcplus_assoc' : Assoc (=) Qcplus
:= Qcplus_assoc.
(* stdpp/numbers.v *)
Instance Qcplus_comm' : Comm (=) Qcplus
:= Qcplus_comm.
(* stdpp/numbers.v *)
Instance Qcplus_left_id : LeftId (=) 0 Qcplus
:= Qcplus_0_l.
(* stdpp/numbers.v *)
Instance Qcplus_right_id : RightId (=) 0 Qcplus
:= Qcplus_0_r.
(* stdpp/numbers.v *)
Instance Qcminus_right_id : RightId (=) 0 Qcminus.
Proof. unfold RightId. intros. ring. Qed.
(* stdpp/numbers.v *)
Instance Qcmult_assoc' : Assoc (=) Qcmult
:= Qcmult_assoc.
(* stdpp/numbers.v *)
Instance Qcmult_comm' : Comm (=) Qcmult
:= Qcmult_comm.
(* stdpp/numbers.v *)
Instance Qcmult_left_id : LeftId (=) 1 Qcmult
:= Qcmult_1_l.
(* stdpp/numbers.v *)
Instance Qcmult_right_id : RightId (=) 1 Qcmult
:= Qcmult_1_r.
(* stdpp/numbers.v *)
Instance Qcmult_left_absorb : LeftAbsorb (=) 0 Qcmult
:= Qcmult_0_l.
(* stdpp/numbers.v *)
Instance Qcmult_right_absorb : RightAbsorb (=) 0 Qcmult
:= Qcmult_0_r.
(* stdpp/numbers.v *)
Instance Qcdiv_right_id : RightId (=) 1 Qcdiv.
Proof. intros x. rewrite <-(Qcmult_1_l (x / 1)), Qcmult_div_r; done. Qed.
(* stdpp/numbers.v *)
Lemma inject_Z_Qred n : Qred (inject_Z n) = inject_Z n.
Proof. apply Qred_identity; auto using Z.gcd_1_r. Qed.
(* stdpp/numbers.v *)
Definition Qc_of_Z (n : Z) : Qc
:= Qcmake _ (inject_Z_Qred n).
(* stdpp/numbers.v *)
Instance Qc_eq_dec: EqDecision Qc
:= Qc_eq_dec.
(* stdpp/numbers.v *)
Instance Qc_le_dec: RelDecision Qcle := λ x y,
  if Qclt_le_dec y x then right _ else left _.
Next Obligation. intros x y; apply Qclt_not_le. Qed.
(* stdpp/numbers.v *)
Instance Qc_lt_dec: RelDecision Qclt := λ x y,
  if Qclt_le_dec x y then left _ else right _.
Next Obligation. done. Qed.
(* stdpp/numbers.v *)
Instance Qc_lt_pi x y : ProofIrrel (x < y).
Proof. unfold Qclt. apply _. Qed.
(* stdpp/numbers.v *)
Instance Qc_le_po: PartialOrder (≤).
Proof.
  repeat split; red; [apply Qcle_refl | apply Qcle_trans | apply Qcle_antisym].
Qed.
(* stdpp/numbers.v *)
Instance Qc_lt_strict: StrictOrder (<).
Proof.
  split; red; [|apply Qclt_trans].
  intros x Hx. by destruct (Qclt_not_eq x x).
Qed.
(* stdpp/numbers.v *)
Instance Qc_le_total: Total Qcle.
Proof. intros x y. destruct (Qclt_le_dec x y); auto using Qclt_le_weak. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_diag x : (x + x)%Qc = (2 * x)%Qc.
Proof. ring. Qed.
(* stdpp/numbers.v *)
Lemma Qcle_ngt (x y : Qc) : x ≤ y ↔ ¬y < x.
Proof. split; auto using Qcle_not_lt, Qcnot_lt_le. Qed.
(* stdpp/numbers.v *)
Lemma Qclt_nge (x y : Qc) : x < y ↔ ¬y ≤ x.
Proof. split; auto using Qclt_not_le, Qcnot_le_lt. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_le_mono_l (x y z : Qc) : x ≤ y ↔ z + x ≤ z + y.
Proof.
  split; intros.
  - by apply Qcplus_le_compat.
  - replace x with ((0 - z) + (z + x)) by ring.
    replace y with ((0 - z) + (z + y)) by ring.
    by apply Qcplus_le_compat.
Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_le_mono_r (x y z : Qc) : x ≤ y ↔ x + z ≤ y + z.
Proof. rewrite !(Qcplus_comm _ z). apply Qcplus_le_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_lt_mono_l (x y z : Qc) : x < y ↔ z + x < z + y.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_lt_mono_r (x y z : Qc) : x < y ↔ x + z < y + z.
Proof. by rewrite !Qclt_nge, <-Qcplus_le_mono_r. Qed.
(* stdpp/numbers.v *)
Instance Qcopp_inj : Inj (=) (=) Qcopp.
Proof.
  intros x y H. by rewrite <-(Qcopp_involutive x), H, Qcopp_involutive.
Qed.
(* stdpp/numbers.v *)
Instance Qcplus_inj_r z : Inj (=) (=) (Qcplus z).
Proof.
  intros x y H. by apply (anti_symm (≤));rewrite (Qcplus_le_mono_l _ _ z), H.
Qed.
(* stdpp/numbers.v *)
Instance Qcplus_inj_l z : Inj (=) (=) (λ x, x + z).
Proof.
  intros x y H. by apply (anti_symm (≤)); rewrite (Qcplus_le_mono_r _ _ z), H.
Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_pos_nonneg (x y : Qc) : 0 < x → 0 ≤ y → 0 < x + y.
Proof.
  intros. apply Qclt_le_trans with (x + 0); [by rewrite Qcplus_0_r|].
  by apply Qcplus_le_mono_l.
Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_nonneg_pos (x y : Qc) : 0 ≤ x → 0 < y → 0 < x + y.
Proof. rewrite (Qcplus_comm x). auto using Qcplus_pos_nonneg. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_pos_pos (x y : Qc) : 0 < x → 0 < y → 0 < x + y.
Proof. auto using Qcplus_pos_nonneg, Qclt_le_weak. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_nonneg_nonneg (x y : Qc) : 0 ≤ x → 0 ≤ y → 0 ≤ x + y.
Proof.
  intros. trans (x + 0); [by rewrite Qcplus_0_r|].
  by apply Qcplus_le_mono_l.
Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_neg_nonpos (x y : Qc) : x < 0 → y ≤ 0 → x + y < 0.
Proof.
  intros. apply Qcle_lt_trans with (x + 0); [|by rewrite Qcplus_0_r].
  by apply Qcplus_le_mono_l.
Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_nonpos_neg (x y : Qc) : x ≤ 0 → y < 0 → x + y < 0.
Proof. rewrite (Qcplus_comm x). auto using Qcplus_neg_nonpos. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_neg_neg (x y : Qc) : x < 0 → y < 0 → x + y < 0.
Proof. auto using Qcplus_nonpos_neg, Qclt_le_weak. Qed.
(* stdpp/numbers.v *)
Lemma Qcplus_nonpos_nonpos (x y : Qc) : x ≤ 0 → y ≤ 0 → x + y ≤ 0.
Proof.
  intros. trans (x + 0); [|by rewrite Qcplus_0_r].
  by apply Qcplus_le_mono_l.
Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_le_mono_nonneg_l x y z : 0 ≤ z → x ≤ y → z * x ≤ z * y.
Proof. intros. rewrite !(Qcmult_comm z). by apply Qcmult_le_compat_r. Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_le_mono_nonneg_r x y z : 0 ≤ z → x ≤ y → x * z ≤ y * z.
Proof. intros. by apply Qcmult_le_compat_r. Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_le_mono_pos_l x y z : 0 < z → x ≤ y ↔ z * x ≤ z * y.
Proof.
  split; auto using Qcmult_le_mono_nonneg_l, Qclt_le_weak.
  rewrite !Qcle_ngt, !(Qcmult_comm z).
  intuition auto using Qcmult_lt_compat_r.
Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_le_mono_pos_r x y z : 0 < z → x ≤ y ↔ x * z ≤ y * z.
Proof. rewrite !(Qcmult_comm _ z). by apply Qcmult_le_mono_pos_l. Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_lt_mono_pos_l x y z : 0 < z → x < y ↔ z * x < z * y.
Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_l. Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_lt_mono_pos_r x y z : 0 < z → x < y ↔ x * z < y * z.
Proof. intros. by rewrite !Qclt_nge, <-Qcmult_le_mono_pos_r. Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_pos_pos x y : 0 < x → 0 < y → 0 < x * y.
Proof.
  intros. apply Qcle_lt_trans with (0 * y); [by rewrite Qcmult_0_l|].
  by apply Qcmult_lt_mono_pos_r.
Qed.
(* stdpp/numbers.v *)
Lemma Qcmult_nonneg_nonneg x y : 0 ≤ x → 0 ≤ y → 0 ≤ x * y.
Proof.
  intros. trans (0 * y); [by rewrite Qcmult_0_l|].
  by apply Qcmult_le_mono_nonneg_r.
Qed.
(* stdpp/numbers.v *)
Lemma Qcinv_pos x : 0 < x → 0 < /x.
Proof.
  intros. assert (0 ≠ x) by (by apply Qclt_not_eq).
  by rewrite (Qcmult_lt_mono_pos_r _ _ x), Qcmult_0_l, Qcmult_inv_l by done.
Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_0 : Qc_of_Z 0 = 0.
Proof. by apply Qc_is_canon. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_1 : Qc_of_Z 1 = 1.
Proof. by apply Qc_is_canon. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_2 : Qc_of_Z 2 = 2.
Proof. by apply Qc_is_canon. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj n m : Qc_of_Z n = Qc_of_Z m → n = m.
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_iff n m : Qc_of_Z n = Qc_of_Z m ↔ n = m.
Proof. split; [ auto using Z2Qc_inj | by intros -> ]. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_le n m : (n ≤ m)%Z ↔ Qc_of_Z n ≤ Qc_of_Z m.
Proof. by rewrite Zle_Qle. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_lt n m : (n < m)%Z ↔ Qc_of_Z n < Qc_of_Z m.
Proof. by rewrite Zlt_Qlt. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_add n m : Qc_of_Z (n + m) = Qc_of_Z n + Qc_of_Z m.
Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_plus. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_mul n m : Qc_of_Z (n * m) = Qc_of_Z n * Qc_of_Z m.
Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_mult. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_opp n : Qc_of_Z (-n) = -Qc_of_Z n.
Proof. apply Qc_is_canon; simpl. by rewrite Qred_correct, inject_Z_opp. Qed.
(* stdpp/numbers.v *)
Lemma Z2Qc_inj_sub n m : Qc_of_Z (n - m) = Qc_of_Z n - Qc_of_Z m.
Proof.
  apply Qc_is_canon; simpl.
  by rewrite !Qred_correct, <-inject_Z_opp, <-inject_Z_plus.
Qed.
(* stdpp/numbers.v *)
Record Qp
:= mk_Qp { Qp_to_Qc : Qc ; Qp_prf : (0 < Qp_to_Qc)%Qc }.
(* stdpp/numbers.v *)
Definition pos_to_Qp (n : positive) : Qp := mk_Qp (Qc_of_Z $ Z.pos n) _.
Next Obligation. intros n. by rewrite <-Z2Qc_inj_0, <-Z2Qc_inj_lt. Qed.
(* stdpp/numbers.v *)
Lemma to_Qc_inj_iff p q : Qp_to_Qc p = Qp_to_Qc q ↔ p = q.
Proof.
    split; [|by intros ->].
    destruct p, q; intros; simplify_eq/=; f_equal; apply (proof_irrel _).
  Qed.
(* stdpp/numbers.v *)
Instance eq_dec : EqDecision Qp.
Proof.
    refine (λ p q, cast_if (decide (Qp_to_Qc p = Qp_to_Qc q)));
      abstract (by rewrite <-to_Qc_inj_iff).
  Defined.
(* stdpp/numbers.v *)
Definition add (p q : Qp) : Qp
:=
    let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
    mk_Qp (p + q) (Qcplus_pos_pos _ _ Hp Hq).
(* stdpp/numbers.v *)
Definition sub (p q : Qp) : option Qp
:=
    let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
    let pq := (p - q)%Qc in
    Hpq ← guard (0 < pq)%Qc; Some (mk_Qp pq Hpq).
(* stdpp/numbers.v *)
Definition mul (p q : Qp) : Qp
:=
    let 'mk_Qp p Hp := p in let 'mk_Qp q Hq := q in
    mk_Qp (p * q) (Qcmult_pos_pos _ _ Hp Hq).
(* stdpp/numbers.v *)
Definition inv (q : Qp) : Qp
:=
    let 'mk_Qp q Hq := q return _ in
    mk_Qp (/ q)%Qc (Qcinv_pos _ Hq).
(* stdpp/numbers.v *)
Definition div (p q : Qp) : Qp
:= mul p (inv q).
(* stdpp/numbers.v *)
Definition le (p q : Qp) : Prop
:=
    let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p ≤ q)%Qc.
(* stdpp/numbers.v *)
Definition lt (p q : Qp) : Prop
:=
    let 'mk_Qp p _ := p in let 'mk_Qp q _ := q in (p < q)%Qc.