proposition: Lemma Rplus_diag : forall r, r + r = 2 * r.
proof: Proof. intros r; replace 2 with (1 + 1) by reflexivity. now rewrite Rmult_plus_distr_r, Rmult_1_l. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField