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