proposition: Theorem Rplus_cancel_l : forall n m p : R, p + n == p + m <-> n == m.
proof: Proof. intros n m p; split; intro H. - setoid_replace n with (- p + (p + n)) by ring. setoid_replace m with (- p + (p + m)) by ring. now rewrite H. - now rewrite H. Qed.
imports: Setoid Ring