proposition: Lemma gen_phiPOS_inj x y : gen_phiPOS rI radd rmul x == gen_phiPOS rI radd rmul y -> x = y.
proof: Proof. rewrite <- !(same_gen Rsth Reqe ARth). case (Pos.compare_spec x y). - intros. trivial. - intros. elim gen_phiPOS_not_0 with (y - x)%positive. apply add_inj_r with x. symmetry. rewrite (ARadd_0_r Rsth ARth). rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth). now rewrite Pos.add_comm, Pos.sub_add. - intros. elim gen_phiPOS_not_0 with (x - y)%positive. apply add_inj_r with y. rewrite (ARadd_0_r Rsth ARth). rewrite <- (ARgen_phiPOS_add Rsth Reqe ARth). now rewrite Pos.add_comm, Pos.sub_add. Qed.
imports: ZArith_base