proposition: Lemma Q_average_between@{} : forall q r : Q, q < r -> q < (q + r) / 2 < r.
proof: Proof. intros q r E. split. - apply flip_pos_minus. assert (Hrw : (q + r) / 2 - q = (r - q) / 2);[|rewrite Hrw;clear Hrw]. { path_via ((q + r) / 2 - 2 / 2 * q). { rewrite dec_recip_inverse;[|solve_propholds]. rewrite mult_1_l;trivial. } ring_tac.ring_with_integers (NatPair.Z nat). } apply pos_mult_compat;[|apply _]. red. apply (snd (flip_pos_minus _ _)). trivial. - apply flip_pos_minus. assert (Hrw : r - (q + r) / 2 = (r - q) / 2);[|rewrite Hrw;clear Hrw]. { path_via (2 / 2 * r - (q + r) / 2). { rewrite dec_recip_inverse;[|solve_propholds]. rewrite mult_1_l;trivial. } ring_tac.ring_with_integers (NatPair.Z nat). } apply pos_mult_compat;[|apply _]. red. apply (snd (flip_pos_minus _ _)). trivial. 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