proposition: Lemma Length_Intrvl : forall (x : R1) (n : nat), Length _ (Intrvl x n)[=](Two [/]ThreeNZ)[^]n[*](start_r x[-]start_l x).
proof: Proof. intros. induction n as [| n Hrecn]. unfold Length in |- *. simpl in |- *. rational. astepr (Two [/]ThreeNZ[*]((Two [/]ThreeNZ)[^]n[*](start_r x[-]start_l x))). astepr (Two [/]ThreeNZ[*]Length Q_as_COrdField (Intrvl x n)). apply delta_Intrvl. astepr ((Two [/]ThreeNZ)[^]n[*]Two [/]ThreeNZ[*](start_r x[-]start_l x)). rational. Qed.
imports: CoRN.reals.Q_in_CReals