proposition: Lemma pred_of_power : forall b e, pred (power (S b) (S e)) = (power (S b) e)*b + pred (power (S b) e).
proof: Proof. simpl. intros;generalize ((S b) ^e). destruct n. simpl. rewrite Nat.mul_0_r. simpl;auto. rewrite (Nat.mul_comm b (S n)). simpl. ring. Qed.
imports: Coq(Arith Lia )