proposition: Lemma module_reel : forall x : R, module (Rinj x) = Rabs x.
proof: Proof. unfold Rinj in |- *; intros. rewrite (passage_algebrique_module (z:=cons_cart x 0) (x:=x) (y:=0)); auto with geo. replace (Rsqr x + Rsqr 0) with (Rsqr x) by (unfold Rsqr; ring). rewrite sqrt_Rsqr_abs; auto. Qed.