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