proposition: Lemma mag_minus : forall x y, (0 < y)%R -> (y < x)%R -> (mag (x - y) <= mag x)%Z.
proof: Proof. intros x y Py Hxy. assert (Px : (0 < x)%R) by apply (Rlt_trans _ _ _ Py Hxy). apply mag_le. - now apply Rlt_Rminus. - rewrite <- (Rplus_0_r x) at 2. apply Rplus_le_compat_l. rewrite <- Ropp_0. now apply Ropp_le_contravar; apply Rlt_le. Qed.
imports: Coq(Psatz Reals ZArith) Zaux