proposition: Lemma plus_INR : forall n m, INR (n + m) = INR n + INR m.
proof: Proof. intros n m; induction m as [| m IHm]. - now rewrite Nat.add_0_r, INR_0, Rplus_0_r. - now rewrite Nat.add_succ_r, 2S_INR, IHm, Rplus_assoc. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField