phanerozoic/Coq-Stdpp huggingface dataset:
(* stdpp/numbers.v *)
Lemma to_Qc_inj_add p q : Qp_to_Qc (add p q) = (Qp_to_Qc p + Qp_to_Qc q)%Qc.
Proof. by destruct p, q. Qed.
(* stdpp/numbers.v *)
Lemma to_Qc_inj_mul p q : Qp_to_Qc (mul p q) = (Qp_to_Qc p * Qp_to_Qc q)%Qc.
Proof. by destruct p, q. Qed.
(* stdpp/numbers.v *)
Lemma to_Qc_inj_le p q : le p q ↔ (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc.
Proof. by destruct p, q. Qed.
(* stdpp/numbers.v *)
Lemma to_Qc_inj_lt p q : lt p q ↔ (Qp_to_Qc p < Qp_to_Qc q)%Qc.
Proof. by destruct p, q. Qed.
(* stdpp/numbers.v *)
Instance le_dec : RelDecision le.
Proof.
    refine (λ p q, cast_if (decide (Qp_to_Qc p ≤ Qp_to_Qc q)%Qc));
      abstract (by rewrite to_Qc_inj_le).
  Defined.
(* stdpp/numbers.v *)
Instance lt_dec : RelDecision lt.
Proof.
    refine (λ p q, cast_if (decide (Qp_to_Qc p < Qp_to_Qc q)%Qc));
      abstract (by rewrite to_Qc_inj_lt).
  Defined.
(* stdpp/numbers.v *)
Instance lt_pi p q : ProofIrrel (lt p q).
Proof. destruct p, q; apply _. Qed.
(* stdpp/numbers.v *)
Definition max (q p : Qp) : Qp
:= if decide (le q p) then p else q.
(* stdpp/numbers.v *)
Definition min (q p : Qp) : Qp
:= if decide (le q p) then q else p.
(* stdpp/numbers.v *)
Notation "/ q"
:= (inv q) : Qp_scope.
(* stdpp/numbers.v *)
Notation "1"
:= (pos_to_Qp 1) : Qp_scope.
(* stdpp/numbers.v *)
Notation "2"
:= (pos_to_Qp 2) : Qp_scope.
(* stdpp/numbers.v *)
Notation "3"
:= (pos_to_Qp 3) : Qp_scope.
(* stdpp/numbers.v *)
Notation "4"
:= (pos_to_Qp 4) : Qp_scope.
(* stdpp/numbers.v *)
Notation "p ≤ q ≤ r"
:= (p ≤ q ∧ q ≤ r) : Qp_scope.
(* stdpp/numbers.v *)
Notation "p ≤ q < r"
:= (p ≤ q ∧ q < r) : Qp_scope.
(* stdpp/numbers.v *)
Notation "p < q < r"
:= (p < q ∧ q < r) : Qp_scope.
(* stdpp/numbers.v *)
Notation "p < q ≤ r"
:= (p < q ∧ q ≤ r) : Qp_scope.
(* stdpp/numbers.v *)
Notation "p ≤ q ≤ r ≤ r'"
:= (p ≤ q ∧ q ≤ r ∧ r ≤ r') : Qp_scope.
(* stdpp/numbers.v *)
Notation "(≤)"
:= le (only parsing) : Qp_scope.
(* stdpp/numbers.v *)
Notation "(<)"
:= lt (only parsing) : Qp_scope.
(* stdpp/numbers.v *)
Instance inhabited : Inhabited Qp
:= populate 1.
(* stdpp/numbers.v *)
Instance add_assoc : Assoc (=) add.
Proof. intros [p ?] [q ?] [r ?]; apply to_Qc_inj_iff, Qcplus_assoc. Qed.
(* stdpp/numbers.v *)
Instance add_comm : Comm (=) add.
Proof. intros [p ?] [q ?]; apply to_Qc_inj_iff, Qcplus_comm. Qed.
(* stdpp/numbers.v *)
Instance add_inj_r p : Inj (=) (=) (add p).
Proof.
    destruct p as [p ?].
    intros [q1 ?] [q2 ?]. rewrite <-!to_Qc_inj_iff; simpl. apply (inj (Qcplus p)).
  Qed.
(* stdpp/numbers.v *)
Instance add_inj_l p : Inj (=) (=) (λ q, q + p).
Proof.
    destruct p as [p ?].
    intros [q1 ?] [q2 ?]. rewrite <-!to_Qc_inj_iff; simpl. apply (inj (λ q, q + p)%Qc).
  Qed.
(* stdpp/numbers.v *)
Instance mul_assoc : Assoc (=) mul.
Proof. intros [p ?] [q ?] [r ?]. apply Qp.to_Qc_inj_iff, Qcmult_assoc. Qed.
(* stdpp/numbers.v *)
Instance mul_comm : Comm (=) mul.
Proof. intros [p ?] [q ?]; apply Qp.to_Qc_inj_iff, Qcmult_comm. Qed.
(* stdpp/numbers.v *)
Instance mul_inj_r p : Inj (=) (=) (mul p).
Proof.
    destruct p as [p ?]. intros [q1 ?] [q2 ?]. rewrite <-!Qp.to_Qc_inj_iff; simpl.
    intros Hpq.
    apply (anti_symm Qcle); apply (Qcmult_le_mono_pos_l _ _ p); by rewrite ?Hpq.
  Qed.
(* stdpp/numbers.v *)
Instance mul_inj_l p : Inj (=) (=) (λ q, q * p).
Proof.
    intros q1 q2 Hpq. apply (inj (mul p)). by rewrite !(comm_L mul p).
  Qed.
(* stdpp/numbers.v *)
Lemma mul_add_distr_l p q r : p * (q + r) = p * q + p * r.
Proof. destruct p, q, r; by apply Qp.to_Qc_inj_iff, Qcmult_plus_distr_r. Qed.
(* stdpp/numbers.v *)
Lemma mul_add_distr_r p q r : (p + q) * r = p * r + q * r.
Proof. destruct p, q, r; by apply Qp.to_Qc_inj_iff, Qcmult_plus_distr_l. Qed.
(* stdpp/numbers.v *)
Lemma mul_1_l p : 1 * p = p.
Proof. destruct p; apply Qp.to_Qc_inj_iff, Qcmult_1_l. Qed.
(* stdpp/numbers.v *)
Lemma mul_1_r p : p * 1 = p.
Proof. destruct p; apply Qp.to_Qc_inj_iff, Qcmult_1_r. Qed.
(* stdpp/numbers.v *)
Instance mul_left_id : LeftId (=) 1 mul
:= mul_1_l.
(* stdpp/numbers.v *)
Instance mul_right_id : RightId (=) 1 mul
:= mul_1_r.
(* stdpp/numbers.v *)
Lemma add_1_1 : 1 + 1 = 2.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma add_diag p : p + p = 2 * p.
Proof. by rewrite <-add_1_1, mul_add_distr_r, !mul_1_l. Qed.
(* stdpp/numbers.v *)
Lemma mul_inv_l p : /p * p = 1.
Proof.
    destruct p as [p ?]; apply Qp.to_Qc_inj_iff; simpl.
    by rewrite Qcmult_inv_l, Z2Qc_inj_1 by (by apply not_symmetry, Qclt_not_eq).
  Qed.
(* stdpp/numbers.v *)
Lemma mul_inv_r p : p * /p = 1.
Proof. by rewrite (comm_L mul), mul_inv_l. Qed.
(* stdpp/numbers.v *)
Lemma inv_mul_distr p q : /(p * q) = /p * /q.
Proof.
    apply (inj (mul (p * q))).
    rewrite mul_inv_r, (comm_L mul p), <-(assoc_L _), (assoc_L mul p).
    by rewrite mul_inv_r, mul_1_l, mul_inv_r.
  Qed.
(* stdpp/numbers.v *)
Lemma inv_involutive p : / /p = p.
Proof.
    rewrite <-(mul_1_l (/ /p)), <-(mul_inv_r p), <-(assoc_L _).
    by rewrite mul_inv_r, mul_1_r.
  Qed.
(* stdpp/numbers.v *)
Instance inv_inj : Inj (=) (=) inv.
Proof.
    intros p1 p2 Hp. apply (inj (mul (/p1))).
    by rewrite mul_inv_l, Hp, mul_inv_l.
  Qed.
(* stdpp/numbers.v *)
Lemma inv_1 : /1 = 1.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma inv_half_half : /2 + /2 = 1.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma inv_quarter_quarter : /4 + /4 = /2.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma div_diag p : p / p = 1.
Proof. apply mul_inv_r. Qed.
(* stdpp/numbers.v *)
Lemma mul_div_l p q : (p / q) * q = p.
Proof. unfold div. by rewrite <-(assoc_L _), mul_inv_l, mul_1_r. Qed.
(* stdpp/numbers.v *)
Lemma mul_div_r p q : q * (p / q) = p.
Proof. by rewrite (comm_L mul q), mul_div_l. Qed.
(* stdpp/numbers.v *)
Lemma div_add_distr p q r : (p + q) / r = p / r + q / r.
Proof. apply mul_add_distr_r. Qed.
(* stdpp/numbers.v *)
Lemma div_div p q r : (p / q) / r = p / (q * r).
Proof. unfold div. by rewrite inv_mul_distr, (assoc_L _). Qed.
(* stdpp/numbers.v *)
Lemma div_mul_cancel_l p q r : (r * p) / (r * q) = p / q.
Proof.
    rewrite <-div_div. f_equiv. unfold div.
    by rewrite (comm_L mul r), <-(assoc_L _), mul_inv_r, mul_1_r.
  Qed.
(* stdpp/numbers.v *)
Lemma div_mul_cancel_r p q r : (p * r) / (q * r) = p / q.
Proof. by rewrite <-!(comm_L mul r), div_mul_cancel_l. Qed.
(* stdpp/numbers.v *)
Lemma div_1 p : p / 1 = p.
Proof. by rewrite <-(mul_1_r (p / 1)), mul_div_l. Qed.
(* stdpp/numbers.v *)
Lemma div_2 p : p / 2 + p / 2 = p.
Proof.
    rewrite <-div_add_distr, add_diag.
    rewrite <-(mul_1_r 2) at 2. by rewrite div_mul_cancel_l, div_1.
  Qed.
(* stdpp/numbers.v *)
Lemma div_2_mul p q : p / (2 * q) + p / (2 * q) = p / q.
Proof. by rewrite <-div_add_distr, add_diag, div_mul_cancel_l. Qed.
(* stdpp/numbers.v *)
Instance div_right_id : RightId (=) 1 div
:= div_1.
(* stdpp/numbers.v *)
Lemma half_half : 1 / 2 + 1 / 2 = 1.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma quarter_quarter : 1 / 4 + 1 / 4 = 1 / 2.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma quarter_three_quarter : 1 / 4 + 3 / 4 = 1.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma three_quarter_quarter : 3 / 4 + 1 / 4 = 1.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Instance div_inj_r p : Inj (=) (=) (div p).
Proof. unfold div; apply _. Qed.
(* stdpp/numbers.v *)
Instance div_inj_l p : Inj (=) (=) (λ q, q / p)%Qp.
Proof. unfold div; apply _. Qed.
(* stdpp/numbers.v *)
Instance le_po : PartialOrder (≤).
Proof.
    split; [split|].
    - intros p. by apply to_Qc_inj_le.
    - intros p q r. rewrite !to_Qc_inj_le. by etrans.
    - intros p q. rewrite !to_Qc_inj_le, <-to_Qc_inj_iff. apply Qcle_antisym.
  Qed.
(* stdpp/numbers.v *)
Instance lt_strict : StrictOrder (<).
Proof.
    split.
    - intros p ?%to_Qc_inj_lt. by apply (irreflexivity (<)%Qc (Qp_to_Qc p)).
    - intros p q r. rewrite !to_Qc_inj_lt. by etrans.
  Qed.
(* stdpp/numbers.v *)
Instance le_total: Total (≤).
Proof. intros p q. rewrite !to_Qc_inj_le. apply (total Qcle). Qed.
(* stdpp/numbers.v *)
Lemma lt_le_incl p q : p < q → p ≤ q.
Proof. rewrite to_Qc_inj_lt, to_Qc_inj_le. apply Qclt_le_weak. Qed.
(* stdpp/numbers.v *)
Lemma le_lteq p q : p ≤ q ↔ p < q ∨ p = q.
Proof.
    rewrite to_Qc_inj_lt, to_Qc_inj_le, <-Qp.to_Qc_inj_iff. split.
    - intros [?| ->]%Qcle_lt_or_eq; auto.
    - intros [?| ->]; auto using Qclt_le_weak.
  Qed.
(* stdpp/numbers.v *)
Lemma lt_ge_cases p q : {p < q} + {q ≤ p}.
Proof.
    refine (cast_if (Qclt_le_dec (Qp_to_Qc p) (Qp_to_Qc q)%Qc));
      [by apply to_Qc_inj_lt|by apply to_Qc_inj_le].
  Defined.
(* stdpp/numbers.v *)
Lemma le_lt_trans p q r : p ≤ q → q < r → p < r.
Proof. rewrite !to_Qc_inj_lt, to_Qc_inj_le. apply Qcle_lt_trans. Qed.
(* stdpp/numbers.v *)
Lemma lt_le_trans p q r : p < q → q ≤ r → p < r.
Proof. rewrite !to_Qc_inj_lt, to_Qc_inj_le. apply Qclt_le_trans. Qed.
(* stdpp/numbers.v *)
Lemma le_ngt p q : p ≤ q ↔ ¬q < p.
Proof.
    rewrite !to_Qc_inj_lt, to_Qc_inj_le.
    split; auto using Qcle_not_lt, Qcnot_lt_le.
  Qed.
(* stdpp/numbers.v *)
Lemma lt_nge p q : p < q ↔ ¬q ≤ p.
Proof.
    rewrite !to_Qc_inj_lt, to_Qc_inj_le.
    split; auto using Qclt_not_le, Qcnot_le_lt.
  Qed.
(* stdpp/numbers.v *)
Lemma add_le_mono_l p q r : p ≤ q ↔ r + p ≤ r + q.
Proof. rewrite !to_Qc_inj_le. destruct p, q, r; apply Qcplus_le_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma add_le_mono_r p q r : p ≤ q ↔ p + r ≤ q + r.
Proof. rewrite !(comm_L add _ r). apply add_le_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma add_le_mono q p n m : q ≤ n → p ≤ m → q + p ≤ n + m.
Proof. intros. etrans; [by apply add_le_mono_l|by apply add_le_mono_r]. Qed.
(* stdpp/numbers.v *)
Lemma add_lt_mono_l p q r : p < q ↔ r + p < r + q.
Proof. by rewrite !lt_nge, <-add_le_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma add_lt_mono_r p q r : p < q ↔ p + r < q + r.
Proof. by rewrite !lt_nge, <-add_le_mono_r. Qed.
(* stdpp/numbers.v *)
Lemma add_lt_mono q p n m : q < n → p < m → q + p < n + m.
Proof. intros. etrans; [by apply add_lt_mono_l|by apply add_lt_mono_r]. Qed.
(* stdpp/numbers.v *)
Lemma mul_le_mono_l p q r : p ≤ q ↔ r * p ≤ r * q.
Proof.
    rewrite !to_Qc_inj_le. destruct p, q, r; by apply Qcmult_le_mono_pos_l.
  Qed.
(* stdpp/numbers.v *)
Lemma mul_le_mono_r p q r : p ≤ q ↔ p * r ≤ q * r.
Proof. rewrite !(comm_L mul _ r). apply mul_le_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma mul_le_mono q p n m : q ≤ n → p ≤ m → q * p ≤ n * m.
Proof. intros. etrans; [by apply mul_le_mono_l|by apply mul_le_mono_r]. Qed.
(* stdpp/numbers.v *)
Lemma mul_lt_mono_l p q r : p < q ↔ r * p < r * q.
Proof.
    rewrite !to_Qc_inj_lt. destruct p, q, r; by apply Qcmult_lt_mono_pos_l.
  Qed.
(* stdpp/numbers.v *)
Lemma mul_lt_mono_r p q r : p < q ↔ p * r < q * r.
Proof. rewrite !(comm_L mul _ r). apply mul_lt_mono_l. Qed.
(* stdpp/numbers.v *)
Lemma mul_lt_mono q p n m : q < n → p < m → q * p < n * m.
Proof. intros. etrans; [by apply mul_lt_mono_l|by apply mul_lt_mono_r]. Qed.
(* stdpp/numbers.v *)
Lemma lt_add_l p q : p < p + q.
Proof.
    destruct p as [p ?], q as [q ?]. apply to_Qc_inj_lt; simpl.
    rewrite <- (Qcplus_0_r p) at 1. by rewrite <-Qcplus_lt_mono_l.
  Qed.
(* stdpp/numbers.v *)
Lemma lt_add_r p q : q < p + q.
Proof. rewrite (comm_L add). apply lt_add_l. Qed.
(* stdpp/numbers.v *)
Lemma not_add_le_l p q : ¬(p + q ≤ p).
Proof. apply lt_nge, lt_add_l. Qed.
(* stdpp/numbers.v *)
Lemma not_add_le_r p q : ¬(p + q ≤ q).
Proof. apply lt_nge, lt_add_r. Qed.
(* stdpp/numbers.v *)
Lemma add_id_free q p : q + p ≠ q.
Proof. intro Heq. apply (not_add_le_l q p). by rewrite Heq. Qed.
(* stdpp/numbers.v *)
Lemma le_add_l p q : p ≤ p + q.
Proof. apply lt_le_incl, lt_add_l. Qed.
(* stdpp/numbers.v *)
Lemma le_add_r p q : q ≤ p + q.
Proof. apply lt_le_incl, lt_add_r. Qed.
(* stdpp/numbers.v *)
Lemma sub_Some p q r : p - q = Some r ↔ p = q + r.
Proof.
    destruct p as [p Hp], q as [q Hq], r as [r Hr].
    unfold sub, add; simpl; rewrite <-Qp.to_Qc_inj_iff; simpl. split.
    - intros; simplify_option_eq. unfold Qcminus.
      by rewrite (Qcplus_comm p), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
    - intros ->. unfold Qcminus.
      rewrite <-Qcplus_assoc, (Qcplus_comm r), Qcplus_assoc.
      rewrite Qcplus_opp_r, Qcplus_0_l. simplify_option_eq; [|done].
      f_equal. by apply Qp.to_Qc_inj_iff.
  Qed.
(* stdpp/numbers.v *)
Lemma lt_sum p q : p < q ↔ ∃ r, q = p + r.
Proof.
    destruct p as [p Hp], q as [q Hq]. rewrite to_Qc_inj_lt; simpl.
    split.
    - intros Hlt%Qclt_minus_iff. exists (mk_Qp (q - p) Hlt).
      apply Qp.to_Qc_inj_iff; simpl. unfold Qcminus.
      by rewrite (Qcplus_comm q), Qcplus_assoc, Qcplus_opp_r, Qcplus_0_l.
    - intros [[r ?] ?%Qp.to_Qc_inj_iff]; simplify_eq/=.
      rewrite <-(Qcplus_0_r p) at 1. by apply Qcplus_lt_mono_l.
  Qed.
(* stdpp/numbers.v *)
Lemma sub_None p q : p - q = None ↔ p ≤ q.
Proof.
    rewrite le_ngt, lt_sum, eq_None_not_Some.
    by setoid_rewrite <-sub_Some.
  Qed.
(* stdpp/numbers.v *)
Lemma sub_diag p : p - p = None.
Proof. by apply sub_None. Qed.
(* stdpp/numbers.v *)
Lemma add_sub p q : (p + q) - q = Some p.
Proof. apply sub_Some. by rewrite (comm_L add). Qed.
(* stdpp/numbers.v *)
Lemma inv_lt_mono p q : p < q ↔ /q < /p.
Proof.
    revert p q. cut (∀ p q, p < q → / q < / p).
    { intros help p q. split; [apply help|]. intros.
      rewrite <-(inv_involutive p), <-(inv_involutive q). by apply help. }
    intros p q Hpq. apply (mul_lt_mono_l _ _ q). rewrite mul_inv_r.
    apply (mul_lt_mono_r _ _ p). rewrite <-(assoc_L _), mul_inv_l.
    by rewrite mul_1_l, mul_1_r.
  Qed.
(* stdpp/numbers.v *)
Lemma inv_le_mono p q : p ≤ q ↔ /q ≤ /p.
Proof. by rewrite !le_ngt, inv_lt_mono. Qed.
(* stdpp/numbers.v *)
Lemma div_le_mono_l p q r : q ≤ p ↔ r / p ≤ r / q.
Proof. unfold div. by rewrite <-mul_le_mono_l, inv_le_mono. Qed.
(* stdpp/numbers.v *)
Lemma div_le_mono_r p q r : p ≤ q ↔ p / r ≤ q / r.
Proof. apply mul_le_mono_r. Qed.
(* stdpp/numbers.v *)
Lemma div_lt_mono_l p q r : q < p ↔ r / p < r / q.
Proof. unfold div. by rewrite <-mul_lt_mono_l, inv_lt_mono. Qed.
(* stdpp/numbers.v *)
Lemma div_lt_mono_r p q r : p < q ↔ p / r < q / r.
Proof. apply mul_lt_mono_r. Qed.
(* stdpp/numbers.v *)
Lemma div_lt p q : 1 < q → p / q < p.
Proof. by rewrite (div_lt_mono_l _ _ p), div_1. Qed.
(* stdpp/numbers.v *)
Lemma div_le p q : 1 ≤ q → p / q ≤ p.
Proof. by rewrite (div_le_mono_l _ _ p), div_1. Qed.
(* stdpp/numbers.v *)
Lemma lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'.
Proof.
    revert q1 q2. cut (∀ q1 q2 : Qp, q1 ≤ q2 →
      ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2').
    { intros help q1 q2.
      destruct (lt_ge_cases q2 q1) as [Hlt|Hle]; eauto.
      destruct (help q2 q1) as (q&q1'&q2'&?&?); eauto using lt_le_incl. }
    intros q1 q2 Hq. exists (q1 / 2)%Qp, (q1 / 2)%Qp.
    assert (q1 / 2 < q2) as [q2' ->]%lt_sum.
    { eapply lt_le_trans, Hq. by apply div_lt. }
    eexists; split; [|done]. by rewrite div_2.
  Qed.
(* stdpp/numbers.v *)
Lemma lower_bound_lt q1 q2 : ∃ q : Qp, q < q1 ∧ q < q2.
Proof.
    destruct (lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]).
    exists qmin. split; eapply lt_sum; eauto.
  Qed.
(* stdpp/numbers.v *)
Lemma cross_split a b c d :
    a + b = c + d →
    ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d.
Proof.
    intros H. revert a b c d H. cut (∀ a b c d : Qp,
      a < c → a + b = c + d →
      ∃ ac ad bc bd, ac + ad = a ∧ bc + bd = b ∧ ac + bc = c ∧ ad + bd = d)%Qp.
    { intros help a b c d Habcd.
      destruct (lt_ge_cases a c) as [?|[?| ->]%le_lteq].
      - auto.
      - destruct (help c d a b); [done..|]. naive_solver.
      - apply (inj (add a)) in Habcd as ->.
        destruct (lower_bound a d) as (q&a'&d'&->&->).
        exists a', q, q, d'. repeat split; done || by rewrite (comm_L add). }
    intros a b c d [e ->]%lt_sum. rewrite <-(assoc_L _). intros ->%(inj (add a)).
    destruct (lower_bound a d) as (q&a'&d'&->&->).
    eexists a', q, (q + e)%Qp, d'; split_and?; [by rewrite (comm_L add)|..|done].
    - by rewrite (assoc_L _), (comm_L add e).
    - by rewrite (assoc_L _), (comm_L add a').
  Qed.
(* stdpp/numbers.v *)
Lemma bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2.
Proof.
    destruct (lt_ge_cases r p) as [[q ->]%lt_sum|?].
    { by exists r, q. }
    exists (p / 2)%Qp, (p / 2)%Qp; split.
    + trans p; [|done]. by apply div_le.
    + by rewrite div_2.
  Qed.
(* stdpp/numbers.v *)
Lemma max_spec q p : (q < p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
Proof.
    unfold max.
    destruct (decide (q ≤ p)) as [[?| ->]%le_lteq|?]; [by auto..|].
    right. split; [|done]. by apply lt_le_incl, lt_nge.
  Qed.
(* stdpp/numbers.v *)
Lemma max_spec_le q p : (q ≤ p ∧ q `max` p = p) ∨ (p ≤ q ∧ q `max` p = q).
Proof. destruct (max_spec q p) as [[?%lt_le_incl?]|]; [left|right]; done. Qed.
(* stdpp/numbers.v *)
Instance max_assoc : Assoc (=) max.
Proof.
    intros q p o. unfold max. destruct (decide (q ≤ p)), (decide (p ≤ o));
      try by rewrite ?decide_True by (by etrans).
    rewrite decide_False by done.
    by rewrite decide_False by (apply lt_nge; etrans; by apply lt_nge).
  Qed.
(* stdpp/numbers.v *)
Instance max_comm : Comm (=) max.
Proof.
    intros q p.
    destruct (max_spec_le q p) as [[?->]|[?->]],
      (max_spec_le p q) as [[?->]|[?->]]; done || by apply (anti_symm (≤)).
  Qed.
(* stdpp/numbers.v *)
Lemma max_id q : q `max` q = q.
Proof. by destruct (max_spec q q) as [[_->]|[_->]]. Qed.
(* stdpp/numbers.v *)
Lemma le_max_l q p : q ≤ q `max` p.
Proof. unfold max. by destruct (decide (q ≤ p)). Qed.
(* stdpp/numbers.v *)
Lemma le_max_r q p : p ≤ q `max` p.
Proof. rewrite (comm_L max q). apply le_max_l. Qed.
(* stdpp/numbers.v *)
Lemma max_add q p : q `max` p ≤ q + p.
Proof.
    unfold max.
    destruct (decide (q ≤ p)); [apply le_add_r|apply le_add_l].
  Qed.
(* stdpp/numbers.v *)
Lemma max_lub_l q p o : q `max` p ≤ o → q ≤ o.
Proof. unfold max. destruct (decide (q ≤ p)); [by etrans|done]. Qed.
(* stdpp/numbers.v *)
Lemma max_lub_r q p o : q `max` p ≤ o → p ≤ o.
Proof. rewrite (comm _ q). apply max_lub_l. Qed.
(* stdpp/numbers.v *)
Lemma min_spec q p : (q < p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
Proof.
    unfold min.
    destruct (decide (q ≤ p)) as [[?| ->]%le_lteq|?]; [by auto..|].
    right. split; [|done]. by apply lt_le_incl, lt_nge.
  Qed.
(* stdpp/numbers.v *)
Lemma min_spec_le q p : (q ≤ p ∧ q `min` p = q) ∨ (p ≤ q ∧ q `min` p = p).
Proof. destruct (min_spec q p) as [[?%lt_le_incl ?]|]; [left|right]; done. Qed.
(* stdpp/numbers.v *)
Instance min_assoc : Assoc (=) min.
Proof.
    intros q p o. unfold min.
    destruct (decide (q ≤ p)), (decide (p ≤ o)); eauto using decide_False.
    - by rewrite !decide_True by (by etrans).
    - by rewrite decide_False by (apply lt_nge; etrans; by apply lt_nge).
  Qed.
(* stdpp/numbers.v *)
Instance min_comm : Comm (=) min.
Proof.
    intros q p.
    destruct (min_spec_le q p) as [[?->]|[?->]],
      (min_spec_le p q) as [[? ->]|[? ->]]; done || by apply (anti_symm (≤)).
  Qed.
(* stdpp/numbers.v *)
Lemma min_id q : q `min` q = q.
Proof. by destruct (min_spec q q) as [[_->]|[_->]]. Qed.
(* stdpp/numbers.v *)
Lemma le_min_r q p : q `min` p ≤ p.
Proof. by destruct (min_spec_le q p) as [[?->]|[?->]]. Qed.
(* stdpp/numbers.v *)
Lemma le_min_l p q : p `min` q ≤ p.
Proof. rewrite (comm_L min p). apply le_min_r. Qed.
(* stdpp/numbers.v *)
Lemma min_l_iff q p : q `min` p = q ↔ q ≤ p.
Proof.
    destruct (min_spec_le q p) as [[?->]|[?->]]; [done|].
    split; [by intros ->|]. intros. by apply (anti_symm (≤)).
  Qed.
(* stdpp/numbers.v *)
Lemma min_r_iff q p : q `min` p = p ↔ p ≤ q.
Proof. rewrite (comm_L min q). apply min_l_iff. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_1 : pos_to_Qp 1 = 1.
Proof. compute_done. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_inj n m : pos_to_Qp n = pos_to_Qp m → n = m.
Proof. by injection 1. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_inj_iff n m : pos_to_Qp n = pos_to_Qp m ↔ n = m.
Proof. split; [apply pos_to_Qp_inj|by intros ->]. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_inj_le n m : (n ≤ m)%positive ↔ pos_to_Qp n ≤ pos_to_Qp m.
Proof. rewrite Qp.to_Qc_inj_le; simpl. by rewrite <-Z2Qc_inj_le. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_inj_lt n m : (n < m)%positive ↔ pos_to_Qp n < pos_to_Qp m.
Proof. by rewrite Pos.lt_nle, Qp.lt_nge, <-pos_to_Qp_inj_le. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_add x y : pos_to_Qp x + pos_to_Qp y = pos_to_Qp (x + y).
Proof. apply Qp.to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_add, Z2Qc_inj_add. Qed.
(* stdpp/numbers.v *)
Lemma pos_to_Qp_mul x y : pos_to_Qp x * pos_to_Qp y = pos_to_Qp (x * y).
Proof. apply Qp.to_Qc_inj_iff; simpl. by rewrite Pos2Z.inj_mul, Z2Qc_inj_mul. Qed.
(* stdpp/numbers.v *)
(* [rotate_nat_add base offset len] computes [(base + offset) `mod`
len]. This is useful in combination with the [rotate] function on
lists, since the index [i] of [rotate n l] corresponds to the index
[rotate_nat_add n i (length i)] of the original list. The definition
uses [Z] for consistency with [rotate_nat_sub]. * *)
Definition rotate_nat_add (base offset len : nat) : nat
:=
  Z.to_nat ((Z.of_nat base + Z.of_nat offset) `mod` Z.of_nat len)%Z.
(* stdpp/numbers.v *)
(* [rotate_nat_sub base offset len] is the inverse of [rotate_nat_add
base offset len]. The definition needs to use modulo on [Z] instead of
on nat since otherwise we need the sidecondition [base < len] on
[rotate_nat_sub_add]. * *)
Definition rotate_nat_sub (base offset len : nat) : nat
:=
  Z.to_nat ((Z.of_nat len + Z.of_nat offset - Z.of_nat base) `mod` Z.of_nat len)%Z.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_add_mod base offset len:
  rotate_nat_add base offset len =
  rotate_nat_add (base `mod` len) offset len.
Proof. unfold rotate_nat_add. by rewrite Nat2Z.inj_mod, Zplus_mod_idemp_l. Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_alt base offset len:
  base < len → offset < len →
  rotate_nat_add base offset len =
  if decide (base + offset < len) then base + offset else base + offset - len.
Proof.
  unfold rotate_nat_add. intros ??. case_decide.
  - rewrite Z.mod_small by lia. by rewrite <-Nat2Z.inj_add, Nat2Z.id.
  - rewrite (Z.mod_in_range 1) by lia.
    by rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-Nat2Z.inj_sub,Nat2Z.id by lia.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_sub_alt base offset len:
  base < len → offset < len →
  rotate_nat_sub base offset len =
  if decide (offset < base) then len + offset - base else offset - base.
Proof.
  unfold rotate_nat_sub. intros ??. case_decide.
  - rewrite Z.mod_small by lia.
    by rewrite <-Nat2Z.inj_add, <-Nat2Z.inj_sub, Nat2Z.id by lia.
  - rewrite (Z.mod_in_range 1) by lia.
    rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_0 base len :
  base < len → rotate_nat_add base 0 len = base.
Proof.
  intros ?. unfold rotate_nat_add.
  rewrite Z.mod_small by lia. by rewrite Z.add_0_r, Nat2Z.id.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_sub_0 base len :
  base < len → rotate_nat_sub base base len = 0.
Proof. intros ?. rewrite rotate_nat_sub_alt by done. case_decide; lia. Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_lt base offset len :
  0 < len → rotate_nat_add base offset len < len.
Proof.
  unfold rotate_nat_add. intros ?.
  pose proof (Nat.mod_upper_bound (base + offset) len).
  rewrite Z2Nat.inj_mod, Z2Nat.inj_add, !Nat2Z.id; lia.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_sub_lt base offset len :
  0 < len → rotate_nat_sub base offset len < len.
Proof.
  unfold rotate_nat_sub. intros ?.
  pose proof (Z_mod_lt (Z.of_nat len + Z.of_nat offset - Z.of_nat base) (Z.of_nat len)).
  apply Nat2Z.inj_lt. rewrite Z2Nat.id; lia.
Qed.
(* stdpp/numbers.v *)
Lemma rotate_nat_add_sub base len offset:
  offset < len →
  rotate_nat_add base (rotate_nat_sub base offset len) len = offset.
Proof.
  intros ?. unfold rotate_nat_add, rotate_nat_sub.
  rewrite Z2Nat.id by (apply Z.mod_pos; lia). rewrite Zplus_mod_idemp_r.
  replace (Z.of_nat base + (Z.of_nat len + Z.of_nat offset - Z.of_nat base))%Z
    with (Z.of_nat len + Z.of_nat offset)%Z by lia.
  rewrite (Z.mod_in_range 1) by lia.
  rewrite Z.mul_1_l, <-Nat2Z.inj_add, <-!Nat2Z.inj_sub,Nat2Z.id; lia.
Qed.