locator (x + y). Proof. intros q r ltqr. set (epsilon := (Qpos_diff q r ltqr) / 2). assert (q+'epsilon=r-'epsilon) by (rewrite path_avg_split_diff_l, path_avg_split_diff_r; reflexivity). destruct (tight_bound m epsilon) as [u [ltuy ltyuepsilon]]. set (s := q-u). assert (qsltx : 'q-'s<y). { unfold s. rewrite (preserves_plus q (-u)). rewrite negate_plus_distr. rewrite (associativity ('q) (-'q) (-'(-u))). rewrite plus_negate_r. rewrite plus_0_l. rewrite (preserves_negate u). rewrite negate_involutive. assumption. } assert (sltseps : s<s+' epsilon) by apply ltQposQ. destruct (l s (s+' epsilon) sltseps) as [ltsx|ltxseps]. - apply inl. apply char_plus_left. apply tr; exists s; split; try assumption. rewrite preserves_minus; assumption. - apply inr. apply char_plus_right. apply tr. set (t := s + ' epsilon); exists t. split; try assumption. assert (r-(q-u+(r-q)/2)=u+'epsilon) as ->. { change ((r - q) / 2) with ('epsilon). rewrite negate_plus_distr. rewrite <- negate_swap_l. rewrite (plus_comm (-q) u). rewrite (plus_assoc r (u-q) (-'epsilon)). rewrite (plus_assoc r u (-q)). rewrite (plus_comm r u). rewrite <- (plus_assoc u r (-q)). rewrite <- (plus_assoc u (r-q) (-'epsilon)). rewrite (plus_comm r (-q)). rewrite <- (plus_assoc (-q) r (-'epsilon)). rewrite path_avg_split_diff_r. rewrite <- path_avg_split_diff_l. rewrite (plus_assoc (-q) q ((r-q)/2)). rewrite (plus_negate_l q). rewrite (plus_0_l _). reflexivity. } assumption. Qed.
Require Import