proposition: Fact ex9 x : x ^ 2 - 2 * x + 1 = 0 <-> x = 1.
proof: Proof. split; intros H. set (V := _ - _ + _) in H. assert (H1 : V = (x - 1) * (x - 1)). unfold V; ring. rewrite H1 in H. destruct (Rmult_integral _ _ H); lra. rewrite H; ring. Qed.
imports: Reals Psatz