proposition: Theorem spec_divc x y: [[div x y]] = [[x]] / [[y]].
proof: Proof. unfold div; rewrite spec_mulc; auto. unfold Qcdiv; apply f_equal2 with (f := Qcmult); auto. apply spec_invc; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig