proposition: Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m.
proof: Proof. intros n m HR. destruct (Nat.eq_dec n m) as [E | NE]; [assumption |]. now apply not_INR in NE. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField