Q_average_between@{} : forall q r : Q, q < r -> q < (q + r) / 2 < r. 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.
Require Import Import Quoting.Instances. Import NatPair.Instances.