proposition: Lemma module_opp_un : module (Rinj (-1)) = 1.
proof: Proof. unfold Rinj in |- *. rewrite (passage_algebrique_module (z:=cons_cart (-1) 0) (x:=-1) (y:=0)); auto with geo. replace (Rsqr (-1) + Rsqr 0) with 1 by (unfold Rsqr; ring). exact sqrt_1. Qed.