(q r : Q) : r - ((r - q) / 2) = (r + q) / 2. Proof. pattern r at 1. rewrite <- (mult_1_r r). pattern (1 : Q) at 1. rewrite <- (dec_recip_inverse 2) by solve_propholds. rewrite (associativity r 2 (/2)). rewrite negate_mult_distr_l. rewrite <- (distribute_r (r*2) (-(r-q)) (/2)). rewrite (distribute_l r 1 1). rewrite (mult_1_r r). rewrite (commutativity (r+r) (-(r-q))). rewrite <- negate_swap_r. rewrite <- (associativity q (-r) (r+r)). rewrite (associativity (-r) r r). rewrite (plus_negate_l r). rewrite (plus_0_l r). rewrite (plus_comm q r). reflexivity. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.