proposition: Lemma pow_pos_monotonic : forall p z1 z2, 0<=z1<=z2 -> pow_pos Zmult z1 p <= pow_pos Zmult z2 p.
proof: Proof. intros p z1 z2 z1_le_z2. functional induction (pow_pos Zmult z1 p);simpl in *. destruct z1_le_z2 as [le_z1 z1_le_z2]. apply Zmult_le_compat;try assumption. apply Zmult_le_compat;try assumption. apply pow_pos_pos;auto with zarith. apply pow_pos_pos;auto with zarith. apply Zmult_le_0_compat;apply pow_pos_pos;auto with zarith. apply Zmult_le_compat;try assumption. apply pow_pos_pos;auto with zarith. apply pow_pos_pos;auto with zarith. auto with zarith. Qed.
imports: Coq(ZArith ZArithRing Ring_polynom Bool List FunInd Lia) CoLoR(closure)