proposition: Lemma lR15 : forall k : R, k * k = (1 + - k) * (1 + - k) -> k = / 2.
proof: Proof. intros. cut (2 <> 0); intros. cut (2 * k = 1); intros. replace k with (/ 2 * (2 * k)). rewrite H1. ring. replace (/ 2 * (2 * k)) with (/ 2 * 2 * k). replace (/ 2 * 2) with 1. ring. auto with real. ring. cut ((1 + - k) * (1 + - k) = - (2 * k) + (k * k + 1)); intros. rewrite <- H in H1. cut (2 * k = k * k + 1 + - (k * k)); intros. rewrite H2. ring. pattern (k * k) at 2 in |- *. rewrite H1. replace (- (- (2 * k) + (k * k + 1))) with (2 * k + - (k * k + 1)). ring. ring. ring. lra. Qed.