proposition: Lemma forme_pol_reel_pos : forall x : R, 0 < x -> Rinj x = cons_pol x 0 :>C.
proof: Proof. intros. apply forme_polaire_def; auto with geo. apply reel_non_nul; auto with real. apply module_reel_pos; auto with real. Qed.