proposition: Lemma gen_phiN_inj x y : gen_phiN rO rI radd rmul x == gen_phiN rO rI radd rmul y -> x = y.
proof: Proof. destruct x as [|p]; destruct y as [|p']; simpl; intros H; trivial. - elim gen_phiPOS_not_0 with p'. symmetry . rewrite (same_gen Rsth Reqe ARth); trivial. - elim gen_phiPOS_not_0 with p. rewrite (same_gen Rsth Reqe ARth); trivial. - rewrite gen_phiPOS_inj with (1 := H); trivial. Qed.
imports: ZArith_base