proposition: Theorem mag_le : forall x y, (0 < x)%R -> (x <= y)%R -> (mag x <= mag y)%Z.
proof: Proof. intros x y H0x Hxy. apply mag_le_abs. now apply Rgt_not_eq. rewrite 2!Rabs_pos_eq. exact Hxy. apply Rle_trans with (2 := Hxy). now apply Rlt_le. now apply Rlt_le. Qed.
imports: Coq(Psatz Reals ZArith) Zaux