proposition: Lemma path_avg_split_diff_l (q r : Q) : q + ((r - q) / 2) = (r + q) / 2.
proof: Proof. pattern q at 1. rewrite <- (mult_1_r q). pattern (1 : Q) at 1. rewrite <- (dec_recip_inverse 2) by solve_propholds. rewrite (associativity q 2 (/2)). rewrite <- (distribute_r (q*2) (r-q) (/2)). rewrite (distribute_l q 1 1). rewrite (mult_1_r q). rewrite (commutativity (q+q) (r-q)). rewrite <- (associativity r (-q) (q+q)). rewrite (associativity (-q) q q). rewrite (plus_negate_l q). rewrite (plus_0_l q). 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