proposition: Lemma minusOneNotZero : forall {R : ConstructiveReals}, CRopp R 1 <> 0.
proof: Proof. intros R absurd. pose proof (CRzero_lt_one R). apply (CRplus_lt_compat_l _ (CRopp R 1)) in H. rewrite CRplus_opp_l, CRplus_0_r in H. rewrite absurd in H. exact (CRlt_asym _ _ H H). Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructivePartialFunctions CMTbase