proposition: Lemma pow_pos_div a b p : ~ b == 0 -> pow_pos rmul (a / b) p == pow_pos rmul a p / pow_pos rmul b p.
proof: Proof. intros H. induction p as [p IHp|p IHp|]; simpl; trivial. - rewrite IHp. assert (nz := pow_pos_nz p H). rewrite !rdiv4; trivial. apply field_is_integral_domain; trivial. - rewrite IHp. assert (nz := pow_pos_nz p H). rewrite !rdiv4; trivial. Qed.
imports: ZArith_base