proposition: Theorem power_div_id : forall n : nat, 0 < n -> power_div n n = 1.
proof: Proof. intros n; case n; unfold power_div in |- *; simpl in |- *; auto with arith. intros n1; unfold pdiv in |- *; simpl in |- *. rewrite ominus_id; case n1; simpl in |- *; auto with arith. Qed.
imports: Coq(ArithRing)