Qpos_diff_pr@{} : forall q r E, r = q + ' (Qpos_diff q r E). Proof. intros q r E. change (r = q + (r - q)). abstract ring_tac.ring_with_integers (NatPair.Z nat). Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.