proposition: Lemma aux_Rpos : forall a b : R, a >= 0 -> b >= 0 -> a + b = Rabs (a + - b) -> a = 0 \/ b = 0.
proof: Proof. intros. assert (Rsqr (a + b) = Rsqr (a + - b)). rewrite H1. rewrite <- Rsqr_abs; auto. apply Rmult_integral. assert (4 * (a * b) = 0). RReplace (4 * (a * b)) (2 * a * (2 * b)). RReplace (2 * a) (a + b + (a + - b)). RReplace (2 * b) (a + b - (a + - b)). rewrite Rsqr_plus_minus. rewrite H2; auto with real. assert (4 <> 0); auto with real. elim Rmult_integral with (r1 := 4) (r2 := a * b); [ intros H5; try clear without_div_Od | intros H5; try clear without_div_Od; try exact H5 | auto ]. absurd (4 = 0); auto. Qed.