proposition: Lemma ARgen_phiPOS_mult : forall x y, gen_phiPOS1 (x * y) == gen_phiPOS1 x * gen_phiPOS1 y.
proof: Proof. intros x;induction x as [x IHx|x IHx|];intros;simpl;norm. - rewrite ARgen_phiPOS_add;simpl;rewrite IHx;norm. - rewrite IHx;rrefl. Qed.
imports: Zbool BinInt BinNat Setoid Ring_theory Ring_polynom