proposition: Lemma sym_sub_add_distr (p q r:positive) : (p-(q+r) ≡ p-q-r)%positive.
proof: Proof. destruct (Pos.lt_total (q+r) p). - apply Pos.sub_add_distr, H. - destruct H. subst p. rewrite Pos.sub_diag. rewrite Pos.add_comm, Pos.add_sub. rewrite Pos.sub_diag. reflexivity. rewrite Pos.sub_lt. 2: exact H. rewrite Pos.sub_le. reflexivity. destruct (Pos.lt_total p q). + rewrite Pos.sub_lt. apply Pos.le_1_l. exact H0. + destruct H0. subst q. rewrite Pos.sub_diag. apply Pos.le_1_l. change (Zpos (p-q) <= Zpos r)%Z. rewrite Pos2Z.inj_sub. 2: exact H0. apply (Z.add_le_mono_r _ _ (Zpos q)). ring_simplify. rewrite <- Pos2Z.inj_add. apply Z.lt_le_incl, H. Qed.
imports: Coq.setoid_ring.ArithRing Coq.Bool.Bool Coq.QArith.Qpower Coq.QArith.Qabs CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.CRArith CoRN.model.metric2.Qmetric CoRN.reals.fast.LazyNat CoRN.reals.fast.CRstreams CoRN.metric2.Limit CoRN.model.totalorder.QposMinMax CoRN.classes.Qclasses MathClasses.interfaces.abstract_algebra