proposition: Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
proof: Proof. induction x;rsimpl. - rewrite IHx. destruct x;simpl;norm. - rewrite IHx;destruct x;simpl;norm. - reflexivity. Qed.
imports: ZArith_base Zpow_def BinInt BinNat Setoid BinList BinPos BinNat BinInt Setoid Ncring Ncring_polynom