proposition: Lemma invSuccRealPositive : forall {R : ConstructiveReals} (n : nat), 0 < CR_of_Q R (1# Pos.of_nat (S n)).
proof: Proof. intros R n. apply CR_of_Q_lt. reflexivity. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions