proposition: Lemma Rlt_0_half : forall {R : ConstructiveReals}, 0 < CR_of_Q R (1#2).
proof: Proof. intro R. apply CR_of_Q_lt. reflexivity. Qed.
imports: QArith PeanoNat ArithRing ConstructiveReals ConstructiveAbs ConstructiveSum ConstructivePower ConstructiveLimits