proposition: Lemma power_le_compat : forall x y n, 0<=x -> x<=y -> power x n <= power y n.
proof: Proof. induction n; intros; simpl. lia. apply Zmult_le_compat. hyp. apply IHn; hyp. hyp. apply pos_power. hyp. Qed.
imports: CoLoR(LogicUtil) Coq(Lia)