proposition: Lemma prod_plus_opp_r : forall x : U * V, prod_plus x (prod_opp x) = prod_zero.
proof: Proof. intros x. apply (f_equal2 pair) ; apply plus_opp_r. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub