proposition: Lemma gen_phiZ_inj x y : gen_phiZ rO rI radd rmul ropp x == gen_phiZ rO rI radd rmul ropp y -> x = y.
proof: Proof. destruct x as [|p|p]; destruct y as [|p'|p']; simpl; intros H. - trivial. - elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). symmetry ; trivial. - elim gen_phiPOS_not_0 with p'. rewrite (same_gen Rsth Reqe ARth). rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite <- H. apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_not_0 with p. rewrite (same_gen Rsth Reqe ARth). trivial. - rewrite gen_phiPOS_inject with (1 := H); trivial. - elim gen_phiPOS_discr_sgn with (1 := H). - elim gen_phiPOS_not_0 with p. rewrite (same_gen Rsth Reqe ARth). rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). rewrite H. apply (ARopp_zero Rsth Reqe ARth). - elim gen_phiPOS_discr_sgn with p' p. symmetry ; trivial. - replace p' with p; trivial. apply gen_phiPOS_inject. rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p)). rewrite <- (Ropp_opp Rsth Reqe Rth (gen_phiPOS 1 radd rmul p')). rewrite H; trivial. reflexivity. Qed.
imports: ZArith_base