proposition: Lemma Cpol_2_root_unicity : forall x1 x2 x3 x4, (forall x, (x + x1) * (x + x2) = (x + x3) * (x + x4)) -> (x1 = x3 /\ x2 = x4) \/ (x1 = x4 /\ x2 = x3).
proof: Proof. intros x1 x2 x3 x4 H. assert (H1 : (forall x : C, (x + x1) * (x + x2) = (x + x3) * (x + x4)) -> (forall x, (x1 + x2 - x3 - x4) * x + x1 * x2 - x3 * x4 = 0)). intros H0 x. assert (H1 : ((x + x1) * (x + x2) = (x + x3) * (x + x4) -> (x1 + x2 - x3 - x4) * x + x1 * x2 - x3 * x4 = 0)). intros H1. apply Cminus_diag_eq in H1. ring_simplify in H1. repeat rewrite <- Cmult_add_distr_l in H1. repeat rewrite <- Cmult_minus_distr_l in H1. rewrite Cmult_comm in H1. assumption. apply H1. apply H0. assert (H2 : (x1 + x2 - x3 - x4 = 0 /\ x1 * x2 - x3 * x4 = 0)). apply Pol_degree_1. intros x. replace ((x1 + x2 - x3 - x4) * x + (x1 * x2 - x3 * x4)) with ((x1 + x2 - x3 - x4) * x + x1 * x2 - x3 * x4) by ring. apply H1. intros x0. apply H. destruct H2 as [H0 H2]. assert (H3 : ((-x1 + x1) * (-x1 + x2) = (-x1 + x3) * (-x1 + x4))). apply H. assert (H4 : ((-x2 + x1) * (-x2 + x2) = (-x2 + x3) * (-x2 + x4))). apply H. rewrite Cadd_opp_l in *. destruct (Ceq_dec x2 x1) ; rewrite Cmult_0_l in *; rewrite Cmult_0_r in * ; symmetry in H3 ; symmetry in H4 ; apply Cmult_integral in H3 ; apply Cmult_integral in H4 ; destruct H3 as [H3|H3] ; destruct H4 as [H4|H4] ; rewrite Cadd_comm in * ; apply Cminus_diag_uniq in H3 ; apply Cminus_diag_uniq in H4 ; subst ; ring_simpl ; intuition. Qed.
imports: Complex Cpow_plus