proposition: Lemma pow_pos_strict_pos : forall z p, 0<z -> 0< pow_pos Zmult z p .
proof: Proof. intros z p; functional induction (pow_pos Zmult z p). 3: easy. intros. apply Zmult_lt_0_compat;auto. apply Zmult_lt_0_compat;auto. intros. apply Zmult_lt_0_compat;auto. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)