proposition: Lemma pow_gt_1 n p : 1<n -> 1<n^p.
proof: Proof. intros H. induction p using peano_ind. - now rewrite pow_1_r. - rewrite pow_succ_r. apply lt_trans with (n*1). + now rewrite mul_1_r. + now apply mul_lt_mono_l. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef