proposition: Lemma switch_line_interp : forall (t b : Q) (m : positive) (j : Z), (j < Z.pos m)%Z -> C t b m (Z.pos m - 1- j) == C b t m j.
proof: Proof. intros t b m j H. unfold C. replace (2 * (Z.pos m -1 - j) + 1)%Z with (2 * (Z.pos m - j) - 1)%Z by ring. change (2 * (Z.pos m - j) - 1 # 1) with (inject_Z (2 * (Z.pos m - j) + - 1)%Z). change (2*Z.pos m#1) with ((2#1)*inject_Z (Z.pos m)). change ((2*j +1)#1) with (inject_Z (2*j+1)%Z). do 2 rewrite -> Q.Zplus_Qplus. rewrite -> Q.Zmult_Qmult. change (inject_Z (-1)) with (-1#1). rewrite -> Q.Zmult_Qmult. change (inject_Z 2) with (2#1). unfold Zminus. rewrite -> Q.Zplus_Qplus. change (inject_Z (-j)) with (-inject_Z j). field. apply Q.positive_nonzero_in_Q. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.reals.fast.RasterQ CoRN.reals.fast.Interval CoRN.logic.Classic CoRN.model.totalorder.QposMinMax Coq.QArith.Qabs Coq.QArith.Qround