proposition: Theorem mag_le_abs : forall x y, (x <> 0)%R -> (Rabs x <= Rabs y)%R -> (mag x <= mag y)%Z.
proof: Proof. intros x y H0x Hxy. destruct (mag x) as (ex, Hx). destruct (mag y) as (ey, Hy). simpl. apply bpow_lt_bpow. specialize (Hx H0x). apply Rle_lt_trans with (1 := proj1 Hx). apply Rle_lt_trans with (1 := Hxy). apply Hy. intros Hy'. apply Rlt_not_le with (1 := Rabs_pos_lt _ H0x). apply Rle_trans with (1 := Hxy). rewrite Hy', Rabs_R0. apply Rle_refl. Qed.
imports: Coq(Psatz Reals ZArith) Zaux