proposition: Theorem cond_Ropp_inj : forall b x y, cond_Ropp b x = cond_Ropp b y -> x = y.
proof: Proof. intros b x y H. rewrite <- (cond_Ropp_involutive b x), H. apply cond_Ropp_involutive. Qed.
imports: Coq(Psatz Reals ZArith) Zaux