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