Qpos_lt_min@{} : forall a b : Q+, exists c ca cb : Q+, a = c + ca /\ b = c + cb. Proof. intros. destruct (total le (' a) (' b)) as [E|E]. - apply Qpos_le_lt_min;trivial. - apply Qpos_le_lt_min in E. destruct E as [c [cb [ca [E1 E2]]]]. exists c,ca,cb;auto. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.