Require Import Reals. Open Scope R_scope. Definition A (x:R): R := -2*x+13. Definition B (x: R): R := let y:=x-7 in 3*y. Lemma Run: forall x:R, B(x)=3*x-21. Proof. intros. unfold B. ring. Qed.