proposition: Lemma lower_bound q1 q2 : ∃ q q1' q2', q1 = q + q1' ∧ q2 = q + q2'.
proof: 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.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)