proposition: Lemma lt_mag : forall x y, (0 < y)%R -> (mag x < mag y)%Z -> (x < y)%R.
proof: Proof. intros x y Py. case (Rle_or_lt x 0); intros Px. intros H. now apply Rle_lt_trans with 0%R. destruct (mag x) as (ex, Hex). destruct (mag y) as (ey, Hey). simpl. intro H. destruct Hex as (_,Hex); [now apply Rgt_not_eq|]. destruct Hey as (Hey,_); [now apply Rgt_not_eq|]. rewrite Rabs_right in Hex; [|now apply Rle_ge; apply Rlt_le]. rewrite Rabs_right in Hey; [|now apply Rle_ge; apply Rlt_le]. apply (Rlt_le_trans _ _ _ Hex). apply Rle_trans with (bpow (ey - 1)); [|exact Hey]. now apply bpow_le; lia. Qed.
imports: Coq(Psatz Reals ZArith) Zaux