proposition: Lemma Length_dIntrvl : forall n : nat, Length _ (dIntrvl n)[=](Two [/]ThreeNZ)[^]n[*](dstart_r[-]dstart_l).
proof: Proof. intros. induction n as [| n Hrecn]. unfold Length in |- *. simpl in |- *. rational. astepr (Two [/]ThreeNZ[*]((Two [/]ThreeNZ)[^]n[*](dstart_r[-]dstart_l))). astepr (Two [/]ThreeNZ[*]Length _ (dIntrvl n)). apply delta_dIntrvl. astepr ((Two [/]ThreeNZ)[^]n[*]Two [/]ThreeNZ[*](dstart_r[-]dstart_l)). rational. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon