proposition: Lemma polaire_produit : forall r a : R, r <> 0 -> cons_pol r a = Cmult (Rinj r) (cons_pol 1 a).
proof: Proof. intros. apply egalite_forme_polaire; auto with geo. rewrite Cmult_module; rewrite module_un_trivial; rewrite module_reel; ring_simplify. pattern r at 2 in |- *. rewrite <- (complexe_polaire_module r a); auto with geo. rewrite Cmult_argument; auto with geo. rewrite argument_module_un. rewrite argument_reel_pos; auto with geo. rewrite complexe_polaire_argument; auto with geo. rewrite plus_commutative; auto with geo. cut (r >= 0); intros. change (r > 0) in |- *. elim H0; intros; auto. absurd (r = 0); auto. rewrite <- (complexe_polaire_module r a); auto with geo. Qed.