proposition: Lemma Rplus_sqr_eq_0_l_depr : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
proof: Proof. now intros r1 r2 H; apply Rsqr_0_uniq, (Rplus_eq_0_l _ (r2²)); try easy; apply Rle_0_sqr. Qed.
imports: RelationClasses Raxioms Rpow_def ZArith ZArithRing RealField