proposition: Lemma Pphi_nil : forall p, Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p = match p with | Pc c => c | Pinj _ p => Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p | PX _ _ p => Pphi 0 Zplus Zmult (IDphi (R:=Z)) nil p end.
proof: Proof. destruct p. simpl;unfold IDphi;reflexivity. simpl. rewrite jump_nil;reflexivity. simpl. replace (pow_pos Zmult 0 p2) with 0. ring. clear; induction p2; simpl. 1, 3: reflexivity. rewrite <- IHp2;reflexivity. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)