proposition: Lemma BigQpowerth : power_theory 1 BigQ.mul BigQ.eq Z.of_N BigQ.power.
proof: Proof. constructor. intros. BigQ.qify. replace (BigQ.to_Q r ^ Z.of_N n)%Q with (pow_N 1 Qmult (BigQ.to_Q r) n)%Q by (now destruct n). destruct n. reflexivity. induction p; simpl; auto; rewrite ?BigQ.spec_mul, ?IHp; reflexivity. Qed.
imports: BigZ Field Qfield QSig QMake Orders GenericMinMax