proposition: Lemma Rappart_repr : forall x y:R, Rrepr x # Rrepr y -> (x <> y)%R.
proof: Proof. intros x y [H|H] abs. - destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H). - destruct abs. exact (CRealLt_asym (Rrepr x) (Rrepr x) H H). Qed.
imports: ZArith_base ClassicalDedekindReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveLUB Rdefinitions