proposition: Lemma delta_Intrvl : forall (x : R1) (n : nat), Length _ (Intrvl x (S n))[=]Two [/]ThreeNZ[*]Length _ (Intrvl x n).
proof: Proof. intros. case (if_cotrans_strong x (Intrvl x n)). intro H. elim H. intros H0 H1. simpl in |- *. rewrite H1. unfold Length in |- *. simpl in |- *. rational. intro H. elim H. intros H0 H1. simpl in |- *. rewrite H1. unfold Length in |- *. simpl in |- *. rational. Qed.
imports: CoRN.reals.Q_in_CReals