proposition: Lemma pow_pos_pos : forall z p, 0<=z -> 0<= pow_pos Zmult z p .
proof: Proof. intros z p;functional induction (pow_pos Zmult z p); auto with zarith. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)