proposition: Lemma Rplus_sqr_eq_0 : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.
proof: Proof. assert (E : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0). { intros r1 r2 H; apply Rsqr_0_uniq, Rplus_eq_0_l with (3 := H); now apply Rle_0_sqr. } intros r1 r2 H; split. - now apply (E _ r2). - now rewrite Rplus_comm in H; apply (E _ r1). Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField