proposition: Lemma S_O_plus_INR_depr : forall n, INR (1 + n) = INR 1 + INR n.
proof: Proof. intros [| n']. - now rewrite INR_0, Rplus_0_r, Nat.add_0_r. - rewrite Rplus_comm; reflexivity. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField