proposition: Lemma delta_dIntrvl : forall n : nat, Length _ (dIntrvl (S n))[=]Two [/]ThreeNZ[*]Length _ (dIntrvl n).
proof: Proof. intros. case (dif_cotrans_strong (dIntrvl n)). intro a. elim a. intros H H0. simpl in |- *. rewrite H0. unfold Length in |- *. simpl in |- *. rational. intro a. elim a. intros H H0. simpl in |- *. rewrite H0. unfold Length in |- *. simpl in |- *. rational. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon