proposition: Lemma path_avg_split_diff_r (q r : Q) : r - ((r - q) / 2) = (r + q) / 2.
proof: 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.
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