proposition: Fact ex6 : forall x y, x <> y -> (x * x - y * y) / (x - y) = y + x.
proof: Proof. intros x y Dxy. field. contradict Dxy. assert (Hx : x = (x - y) + y) by ring. rewrite Hx; clear Hx. rewrite Dxy; ring. Qed.
imports: Reals Psatz