proposition: Lemma Pol_degree_1 : forall a b, (forall x, a * x + b = 0) -> (a = 0 /\ b = 0).
proof: Proof. intros. assert (H1 : (a * 0 + b = 0)). apply H. assert (H2 : (a * 1 + b = 0)). apply H. rewrite Cmult_0_r in H1. rewrite Cmult_1_r in H2. rewrite Cadd_0_l in H1. subst. rewrite Cadd_0_r in H2. subst. intuition. Qed.
imports: Complex Cpow_plus