proposition: Lemma gen_phiPOS_discr_sgn x y : ~ gen_phiPOS rI radd rmul x == - gen_phiPOS rI radd rmul y.
proof: Proof. red; intros. apply gen_phiPOS_not_0 with (y + x)%positive. rewrite (ARgen_phiPOS_add Rsth Reqe ARth). transitivity (gen_phiPOS1 1 radd rmul y + - gen_phiPOS1 1 radd rmul y). - apply (Radd_ext Reqe); trivial. + reflexivity. + rewrite (same_gen Rsth Reqe ARth). rewrite (same_gen Rsth Reqe ARth). trivial. - apply (Ropp_def Rth). Qed.
imports: ZArith_base