proposition: Lemma minus_apply : forall (p q : RX) x, (p[-]q) ! x [=] p ! x[-]q ! x.
proof: Proof. intros. astepl (p[+][--]q) ! x. astepr (p ! x[+][--]q ! x). astepl (p ! x[+]( [--]q) ! x). algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational