proposition: Lemma pos_gt_both : forall a b : Q, forall e, a < ' e -> b < ' e -> exists d d', a < ' d /\ b < ' d /\ e = d + d'.
proof: 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.
imports: HoTT.Classes.implementations.peano_naturals HoTT.Classes.implementations.natpair_integers HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.rationals HoTT.Classes.interfaces.orders HoTT.Classes.theory.groups HoTT.Classes.theory.integers HoTT.Classes.theory.dec_fields HoTT.Classes.orders.sum HoTT.Classes.orders.dec_fields HoTT.Classes.orders.lattices HoTT.Classes.theory.additional_operations HoTT.Classes.tactics.ring_quote HoTT.Classes.tactics.ring_tac