pos_recip_through_plus@{} : forall a b c : Q+, a + b = c * (a / c + b / c). Proof. intros. path_via ((a + b) * (c / c)). - rewrite pos_recip_r;apply pos_eq,symmetry,mult_1_r. - apply pos_eq;ring_tac.ring_with_nat. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.