proposition: Lemma R1_neq_R0 : 1 <> 0.
proof: Proof. intro abs. assert (CRealEq 1%CReal 0%CReal). { transitivity (Rrepr 1). - symmetry. replace 1%R with (Rabst 1%CReal). 2: unfold IZR,IPR; rewrite RbaseSymbolsImpl.R1_def; reflexivity. rewrite Rquot2. reflexivity. - transitivity (Rrepr 0). + rewrite abs. reflexivity. + replace 0%R with (Rabst 0%CReal). 2: unfold IZR; rewrite RbaseSymbolsImpl.R0_def; reflexivity. rewrite Rquot2. reflexivity. } pose proof (CRealLt_morph 0%CReal 0%CReal (CRealEq_refl _) 1%CReal 0%CReal H). apply (CRealLt_irrefl 0%CReal). apply H0. apply CRealLt_0_1. Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions