pos_split2@{} : forall e : Q+, e = e / 2 + e / 2. Proof. intros. path_via (e * (2 / 2)). - rewrite pos_recip_r,pos_mult_1_r;reflexivity. - apply pos_eq. change (' e * (2 / 2) = ' e / 2 + ' e / 2). ring_tac.ring_with_nat. Qed.
Require Import Import Quoting.Instances. Import NatPair.Instances.