proposition: Lemma resolution2 : forall x y x' y' : R, x <> 0 -> x = y -> x * x' = y * y' -> x' = y'.
proof: Proof. intros. cut (y <> 0); intros. replace x' with (/ x * x * x'). replace (/ x * x * x') with (/ x * (x * x')). rewrite H1; rewrite H0. replace (/ y * (y * y')) with (/ y * y * y'). replace (/ y * y) with 1. ring. auto with real. ring. ring. replace (/ x * x) with 1. ring. auto with real. rewrite <- H0; auto. Qed.