pos_recip_r'@{} : forall e : Q+, @paths Q (' e / ' e) 1. Proof. intros. change (' (e / e) = 1). rewrite pos_recip_r. reflexivity. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.