forall a b : Q, forall e, a < ' e -> b < ' e -> exists d d', a < ' d /\ b < ' d /\ e = d + d'. Proof. assert (Haux : forall a b : Q, a <= b -> forall e, a < ' e -> b < ' e -> exists d d', a < ' d /\ b < ' d /\ e = d + d'). { intros a b E e E1 E2. pose proof (Q_average_between _ _ (Qlt_join _ 0 _ E2 prop_holds)) as [E3 E4]. exists (mkQpos _ (le_lt_trans _ _ _ (join_ub_r _ _) E3)). unfold cast at 1 4;simpl. exists (Qpos_diff _ _ E4). repeat split. - apply le_lt_trans with b;trivial. apply le_lt_trans with (join b 0);trivial. apply join_ub_l. - apply le_lt_trans with (join b 0);trivial. apply join_ub_l. - apply pos_eq. unfold cast at 2;simpl. unfold cast at 2;simpl. unfold cast at 3;simpl. abstract ring_tac.ring_with_integers (NatPair.Z nat). } intros a b e E1 E2. destruct (total le a b) as [E|E];auto. destruct (Haux _ _ E e) as [d [d' [E3 [E4 E5]]]];trivial. eauto. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.