proposition: Theorem cond_Ropp_mult_r : forall b x y, cond_Ropp b (x * y) = (x * cond_Ropp b y)%R.
proof: Proof. intros [|] x y. apply sym_eq. apply Ropp_mult_distr_r_reverse. apply refl_equal. Qed.
imports: Coq(Psatz Reals ZArith) Zaux