proposition: Lemma Rsqr_inj : forall x y:R, 0 <= x -> 0 <= y -> Rsqr x = Rsqr y -> x = y.
proof: Proof. intros; generalize (Rle_le_eq (Rsqr x) (Rsqr y)); intro; elim H2; intros _ H3; generalize (H3 H1); intro; elim H4; intros; apply Rle_antisym; apply Rsqr_incr_0; assumption. Qed.
imports: Rdefinitions Raxioms RIneq Rbasic_fun