Require Export ZArith. Open Scope Z_scope. Lemma Zsquare_pos: forall z:Z, 0<=z^2. Admitted. (* L'anneau des entiers de Gauss *) Inductive gauss : Set := g : ... Definition g0 := ... Definition g1 := ... Definition gi := ... Definition gadd (n m:gauss) := ... Definition gmult (n m:gauss) := ... Definition gopp (n:gauss) := ... Definition gminus (n m:gauss) := ... Definition gequal (n m:gauss) := (n=m). (* Check (@ring_theory gauss g0 g1 gadd gmult gminus gopp gequal). *) Lemma Radd_0_l : forall x : gauss, gequal (gadd g0 x) x. Proof. Lemma Radd_comm : forall x y : gauss, gequal (gadd x y) (gadd y x). Proof. Lemma Radd_assoc : forall x y z :gauss, gequal (gadd x (gadd y z)) (gadd (gadd x y) z). Proof. Lemma Rmul_1_l : forall x : gauss, gequal (gmult g1 x) x. Proof. Lemma Rmul_comm : forall x y : gauss, gequal (gmult x y) (gmult y x). Proof. Lemma Rmul_assoc : forall x y z : gauss, gequal (gmult x (gmult y z)) (gmult (gmult x y) z). Proof. Lemma Rdistr_l : forall x y z : gauss, gequal (gmult (gadd x y) z) (gadd (gmult x z) (gmult y z)). Proof. Lemma Rsub_def : forall x y : gauss, gequal (gminus x y) (gadd x (gopp y)). Proof. Lemma Ropp_def : forall x : gauss, gequal (gadd x (gopp x)) g0. Proof. Lemma Gth : ring_theory g0 g1 gadd gmult gminus gopp (@eq gauss). Proof. Add Ring A_ring : Gth. Lemma essai : gminus g1 g1=g0. (* bien s'assurer que cet exemple fonctionne *) Proof. ring. Qed. (* conjugate *) Definition conj (n:gauss) := ... Definition real(n:gauss) := ... Definition im(n:gauss) := ... Definition Ng (n:gauss) : gauss := ... Lemma Ng_im : forall n, im (Ng(n))=0%Z. Proof. Lemma Ng_real : forall n, 0%Z <=real(Ng(n)). Proof. Definition N (n: gauss) : Z. ??? Defined. Lemma Ng_multiplicative : forall p q:gauss, Ng (gmult p q) = gmult (Ng p) (Ng q). Proof. Lemma real_gmult : forall x y: gauss, im(x)=0 -> im(y)=0 -> real(gmult x y) = (real x) * (real y). intros x y; case x;case y; simpl. intros; subst; ring. Qed. (* characterizing N w.r.t Ng *) Lemma N_Ng : forall x, N x = real (Ng x). Proof. Lemma N_multiplicative : forall p q:gauss, N (gmult p q) = (N p) * (N q). Proof. Lemma Zsquare_simpl : forall z, z^2=0 -> z=0. Proof. Lemma N_g0 : forall p, N p=0 -> p=g0. Proof. Lemma lambda : forall x k, k*k*(N x)=N (gmult (g k 0) x). Proof. Lemma integral : forall x y:gauss, gmult x y=g0 -> x=g0 \/ y=g0. Proof. (* subgroup *) Fixpoint iter ... Definition units := {x:gauss| x=g1 \/ x=gi\/ x= (gopp g1)\/x=(gopp gi)}. Lemma stable_units : ... Lemma i_generator : forall x:units, exists n:nat, projT1 x=iter (fun x => gmult x gi) n gi. Proof.