proposition: Lemma Ropp_mul_l x y : -(x * y) == -x * y.
proof: Proof. rewrite <-(Radd_0_l Rth (- x * y)). rewrite (Radd_comm Rth), <-(Ropp_def Rth (x*y)). rewrite (Radd_assoc Rth), <- (Rdistr_l Rth). rewrite (Radd_comm Rth (-x)), (Ropp_def Rth). now rewrite Rmul_0_l, (Radd_0_l Rth). Qed.
imports: Setoid Morphisms BinPos BinNat