proposition: Lemma bounded_split p r : ∃ q1 q2 : Qp, q1 ≤ r ∧ p = q1 + q2.
proof: 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.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)