proposition: Lemma mag_sqrt : forall x, (0 < x)%R -> mag (sqrt x) = Z.div2 (mag x + 1) :> Z.
proof: Proof. intros x Px. apply mag_unique. destruct mag as [e He]. simpl. specialize (He (Rgt_not_eq _ _ Px)). rewrite Rabs_pos_eq in He by now apply Rlt_le. split. - rewrite <- (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. apply Rsqr_le_abs_0. rewrite Rsqr_sqrt by now apply Rlt_le. apply Rle_trans with (2 := proj1 He). unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). destruct Z.odd ; intros ; lia. - rewrite <- (Rabs_pos_eq (bpow _)) by apply bpow_ge_0. apply Rsqr_lt_abs_0. rewrite Rsqr_sqrt by now apply Rlt_le. apply Rlt_le_trans with (1 := proj2 He). unfold Rsqr ; rewrite <- bpow_plus. apply bpow_le. generalize (Zdiv2_odd_eqn (e + 1)). destruct Z.odd ; intros ; lia. Qed.
imports: Coq(Psatz Reals ZArith) Zaux