proposition: Lemma same_gen : forall x, gen_phiPOS1 x == gen_phiPOS x.
proof: Proof. intros x;induction x as [x IHx|x IHx|];simpl. - rewrite IHx;destruct x;simpl;norm. - rewrite IHx;destruct x;simpl;norm. - rrefl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom