proposition: Lemma rational_sqrt_scale (n : Z) a : 0 ≤ a → scale ((2#1) ^ n) (rational_sqrt (a * (4#1) ^ (-n))) = rational_sqrt a.
proof: Proof. intros E. rewrite <-CRmult_scale. revert n. apply biinduction. solve_proper. simpl. rewrite Qmult_1_r. now ring_simplify. intros n. setoid_replace ('((2#1) ^ (1 + n)) * rational_sqrt (a * (4#1) ^ -(1 + n)))%CR with ('((2#1) ^ n) * scale (2#1) (rational_sqrt ((a * (4#1) ^ -n) / (4#1))))%CR. assert (Pa1 : [0][<=](inj_Q IR (a * (4#1) ^ (- n)))). stepl (inj_Q IR 0); [| now (apply (inj_Q_nring IR 0))]. apply inj_Q_leEq. apply Qmult_le_0_compat; [assumption|]. now apply Qpower_pos. assert (Pa2 : [0][<=](inj_Q IR (a * (4#1) ^ (- n) / (4 # 1)))). stepl (inj_Q IR 0); [| now (apply (inj_Q_nring IR 0))]. apply inj_Q_leEq. apply Qmult_le_0_compat; [|easy]. apply Qmult_le_0_compat; [assumption|]. now apply Qpower_pos. rewrite (rational_sqrt_correct _ Pa1), (rational_sqrt_correct _ Pa2). split; intros E2; rewrite <-E2; now rewrite rational_sqrt_big_bounded_correct_aux. rewrite Zopp_plus_distr. rewrite <-CRmult_scale. rewrite 2!Qpower_plus by discriminate. simpl. rewrite (Qmult_comm (2#1) ((2#1) ^ n)), <-CRmult_Qmult. rewrite (Qmult_comm (/(4#1))), Qmult_assoc. symmetry. apply associativity. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.Q_in_CReals CoRN.reals.fast.CRpower CoRN.reals.fast.CRArith CoRN.reals.fast.CRIR CoRN.reals.NRootIR CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.model.metric2.Qmetric Coq.QArith.Qpower CoRN.model.ordfields.Qordfield CoRN.reals.fast.Compress Coq.NArith.Ndigits CoRN.reals.fast.PowerBound CoRN.transc.RealPowers CoRN.reals.fast.ContinuousCorrect CoRN.tactics.Qauto CoRN.tactics.CornTac MathClasses.interfaces.abstract_algebra