proposition: Lemma U_minus_V : forall n : nat, U n[-]V n[=]Length _ (dIntrvl n) [/]TwoNZ.
proof: Proof. intros. unfold U in |- *. unfold V in |- *. unfold Length in |- *. rational. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon