proposition: Lemma lower_bound_lt q1 q2 : ∃ q : Qp, q < q1 ∧ q < q2.
proof: Proof. destruct (lower_bound q1 q2) as (qmin & q1' & q2' & [-> ->]). exists qmin. split; eapply lt_sum; eauto. Qed.
imports: Coq(QArith Qcanon) stdpp(well_founded) stdpp(options)