proposition: Lemma module_reel_pos : forall x : R, 0 <= x -> module (Rinj x) = 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 in |- *; ring). rewrite sqrt_Rsqr; auto. Qed.