proposition: Lemma Psquare_ok P l : (Psquare P)@l == P@l * P@l.
proof: Proof. revert l;induction P as [|? ? IHP|P2 IHP1 p ? IHP2];simpl;intros l;Esimpl. - apply IHP. - rewrite Padd_ok, Pmul_ok;Esimpl. rewrite IHP1, IHP2. mul_push ((hd l)^p). now mul_push (P2@l). Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory